ocaml 3.09 transition

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

diff --git a/helm/coq-contribs/LAMBDA-TYPES/pr1_confluence.v b/helm/coq-contribs/LAMBDA-TYPES/pr1_confluence.v
index 222a08ceaefea54fa0323f88bac1aa84bb12265b..fac076d31b212c82863a67055a6b2e1aa4820c34 100644 (file)
--- a/helm/coq-contribs/LAMBDA-TYPES/pr1_confluence.v
+++ b/helm/coq-contribs/LAMBDA-TYPES/pr1_confluence.v
@@ -1,3 +1,5 @@
+(*#* #stop file *)
+
 Require pr0_confluence.
 Require pr1_defs.
 
@@ -11,9 +13,6 @@ Require pr1_defs.
 
       Theorem pr1_strip : (t0,t1:?) (pr1 t0 t1) -> (t2:?) (pr0 t0 t2) ->
                           (EX t | (pr1 t1 t) & (pr1 t2 t)).
-
-(*#* #stop proof *)
-
       Intros until 1; XElim H; Intros.
 (* case 1 : pr1_r *)
       XEAuto.
@@ -23,16 +22,11 @@ Require pr1_defs.
       XElim H1; Intros; XEAuto.
       Qed.
 
-(*#* #start proof *)
-
 (*#* #caption "confluence with itself: Church-Rosser property" *)
 (*#* #cap #cap t0, t1, t2, t *)
 
       Theorem pr1_confluence : (t0,t1:?) (pr1 t0 t1) -> (t2:?) (pr1 t0 t2) ->
                                (EX t | (pr1 t1 t) & (pr1 t2 t)).
-
-(*#* #stop file *)
-
       Intros until 1; XElim H; Intros.
 (* case 1 : pr1_r *)
       XEAuto.
@@ -58,7 +52,5 @@ Require pr1_defs.
                XElim H1; Intros
             | _ -> Pr0Confluence.
 
-(*#* #start file *)
-
 (*#* #single *)