some reorganization and some corrections

[helm.git] / helm / coq-contribs / LAMBDA-TYPES / drop_defs.v

diff --git a/helm/coq-contribs/LAMBDA-TYPES/drop_defs.v b/helm/coq-contribs/LAMBDA-TYPES/drop_defs.v
index e1576c50481bc9555557f4ce659168cf3174c84b..022c66f655354f50a518bf7e70ef0cde3621acda 100644 (file)
--- a/helm/coq-contribs/LAMBDA-TYPES/drop_defs.v
+++ b/helm/coq-contribs/LAMBDA-TYPES/drop_defs.v
@@ -1,17 +1,23 @@
-(*#* #stop file *)
-
 Require Export contexts_defs.
 Require Export lift_defs.
 
+(*#* #caption "current axioms for dropping",
+   "base case", "untouched tail item", 
+   "dropped tail item", "updated tail item"
+*)
+(*#* #cap #alpha c in C1, e in C2, u in V, k in z, n in k, d in i, r in q *)
+
       Inductive drop : nat -> nat -> C -> C -> Prop :=
          | drop_sort : (h,d,n:?) (drop h d (CSort n) (CSort n))
-         | drop_tail : (c,e:?) (drop (0) (0) c e) ->
+         | drop_comp : (c,e:?) (drop (0) (0) c e) ->
                        (k:?; u:?) (drop (0) (0) (CTail c k u) (CTail e k u))
          | drop_drop : (k:?; h:?; c,e:?) (drop (r k h) (0) c e) ->
                        (u:?) (drop (S h) (0) (CTail c k u) e)
          | drop_skip : (k:?; h,d:?; c,e:?) (drop h (r k d) c e) -> (u:?)
                        (drop h (S d) (CTail c k (lift h (r k d) u)) (CTail e k u)).
 
+(*#* #stop file *)
+
       Hint drop : ltlc := Constructors drop.
 
       Hint discr : ltlc := Extern 4 (drop ? ? ? ?) Simpl.
@@ -28,7 +34,7 @@ Require Export lift_defs.
       Intros until 1; Repeat InsertEq H '(0); XElim H; Intros.
 (* case 1 : drop_sort *)
       XAuto.
-(* case 2 : drop_tail *)
+(* case 2 : drop_comp *)
       Rewrite H0; XAuto.
 (* case 3 : drop_drop *)
       Inversion H2.
@@ -44,7 +50,7 @@ Require Export lift_defs.
       XElim H; Intros.
 (* case 1 : drop_sort *)
       Inversion H1.
-(* case 2 : drop_tail *)
+(* case 2 : drop_comp *)
       Inversion H1.
 (* case 3 : drop_drop *)
       Inversion H1; Inversion H3.