--- a/src/Tactics.v	Mon Dec 01 08:32:20 2008 -0500
+++ b/src/Tactics.v	Fri Jan 02 08:57:25 2009 -0500
@@ -137,13 +137,13 @@
 
 Ltac crush := crush' false fail.
 
-Theorem dep_destruct : forall (T : Type) (T' : T -> Type) x (v : T' x) (P : T' x -> Prop),
+Theorem dep_destruct : forall (T : Type) (T' : T -> Type) x (v : T' x) (P : T' x -> Type),
   (forall x' (v' : T' x') (Heq : x' = x), P (match Heq in (_ = x) return (T' x) with
                                                | refl_equal => v'
                                              end))
   -> P v.
   intros.
-  generalize (H _ v (refl_equal _)); trivial.
+  generalize (X _ v (refl_equal _)); trivial.
 Qed.
 
 Ltac dep_destruct E :=