X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fcoq-contribs%2FLAMBDA-TYPES%2Fdrop_props.v;h=84c8676fb4c42541a1378cd0bbf23d4f5f13b997;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=c9d3ef294bf9780c81580529b5e2b20ed1a4ee8c;hpb=1b21075e987872a2e3103203b4e67c939e4a9f6a;p=helm.git

diff --git a/helm/coq-contribs/LAMBDA-TYPES/drop_props.v b/helm/coq-contribs/LAMBDA-TYPES/drop_props.v
index c9d3ef294..84c8676fb 100644
--- a/helm/coq-contribs/LAMBDA-TYPES/drop_props.v
+++ b/helm/coq-contribs/LAMBDA-TYPES/drop_props.v
@@ -1,3 +1,5 @@
+(*#* #stop file *)
+
 Require lift_gen.
 Require drop_defs.
 
@@ -5,24 +7,17 @@ Require drop_defs.
 
    Section confluence. (*****************************************************)
 
-(*#* #stop macro *)
-
       Tactic Definition IH :=
          Match Context With
             [ H1: (drop ?1 ?2 c ?3); H2: (drop ?1 ?2 c ?4) |- ? ] ->
                LApply (H ?4 ?2 ?1); [ Clear H H2; Intros H | XAuto ];
                LApply (H ?3); [ Clear H H1; Intros | XAuto ].
 
-(*#* #start macro *)
-
 (*#* #caption "confluence, first case" *)
 (*#* #cap #alpha c in C, x1 in C1, x2 in C2, d in i *)
 
       Theorem drop_mono : (c,x1:?; d,h:?) (drop h d c x1) ->
                           (x2:?) (drop h d c x2) -> x1 = x2.
-
-(*#* #stop proof *)
-
       XElim c.
 (* case 1: CSort *)
       Intros; Repeat DropGenBase; Rewrite H0; XAuto.
@@ -35,8 +30,6 @@ Require drop_defs.
       LiftGen; IH; XAuto.
       Qed.
 
-(*#* #start proof *)
-
 (*#* #caption "confluence, second case" *)
 (*#* #cap #alpha c in C1, c0 in E1, e in C2, e0 in E2, u in V1, v in V2, i in k, d in i *)
 
@@ -47,9 +40,6 @@ Require drop_defs.
                                        (drop i (0) e (CTail e0 (Bind b) v)) &
                                        (drop h d c0 e0)
                             ).
-
-(*#* #stop proof *)
-
       XElim i.
 (* case 1 : i = 0 *)
       Intros until 1.
@@ -72,17 +62,12 @@ Require drop_defs.
       XElim H; XEAuto.
       Qed.
 
-(*#* #start proof *)
-
 (*#* #caption "confluence, third case" *)
 (*#* #cap #alpha c in C, a in C1, e in C2, i in k, d in i *)
 
       Theorem drop_conf_ge: (i:?; a,c:?) (drop i (0) c a) ->
                             (e:?; h,d:?) (drop h d c e) -> (le (plus d h) i) ->
                             (drop (minus i h) (0) e a).
-
-(*#* #stop proof *)
-
       XElim i.
 (* case 1 : i = 0 *)
       Intros until 1.
@@ -119,8 +104,6 @@ Require drop_defs.
       Rewrite <- minus_Sn_m; XEAuto.
       Qed.
 
-(*#* #start proof *)
-
    End confluence.
 
    Section transitivity. (***************************************************)
@@ -132,9 +115,6 @@ Require drop_defs.
                               (c1,c2:?; h:?) (drop h d c1 c2) ->
                               (e2:?) (drop i (0) c2 e2) ->
                               (EX e1 | (drop i (0) c1 e1) & (drop h (minus d i) e1 e2)).
-
-(*#* #stop proof *)
-
       XElim i.
 (* case 1 : i = 0 *)
       Intros.
@@ -165,17 +145,12 @@ Require drop_defs.
       XElim IHc; XEAuto.
       Qed.
 
-(*#* #start proof *)
-
 (*#* #caption "transitivity, second case" *)
 (*#* #cap #alpha c1 in C1, c2 in C, e2 in C2, d in i, i in k *)
 
       Theorem drop_trans_ge : (i:?; c1,c2:?; d,h:?) (drop h d c1 c2) ->
                               (e2:?) (drop i (0) c2 e2) -> (le d i) ->
                               (drop (plus i h) (0) c1 e2).
-
-(*#* #stop proof *)
-
       XElim i.
 (* case 1: i = 0 *)
       Intros.
@@ -203,12 +178,8 @@ Require drop_defs.
       DropGenBase; Apply drop_drop; NewInduction k; Simpl; XEAuto. (**) (* explicit constructor *)
       Qed.
 
-(*#* #start proof *)
-
    End transitivity.
 
-(*#* #stop macro *)
-
       Tactic Definition DropDis :=
          Match Context With
             [ H1: (drop ?1 ?2 ?3 ?4); H2: (drop ?1 ?2 ?3 ?5) |- ? ] ->
@@ -254,6 +225,4 @@ Require drop_defs.
                LApply (H1 ?6); [ Clear H1 H2; Intros H1 | XAuto ];
                LApply H1; [ Clear H1; Intros | XAuto ].
 
-(*#* #start macro *)
-
 (*#* #single *)