X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fcoq-contribs%2FLAMBDA-TYPES%2Fpr1_confluence.v;h=fac076d31b212c82863a67055a6b2e1aa4820c34;hb=97c2d258a5c524eb5c4b85208899d80751a2c82f;hp=222a08ceaefea54fa0323f88bac1aa84bb12265b;hpb=1b21075e987872a2e3103203b4e67c939e4a9f6a;p=helm.git

diff --git a/helm/coq-contribs/LAMBDA-TYPES/pr1_confluence.v b/helm/coq-contribs/LAMBDA-TYPES/pr1_confluence.v
index 222a08cea..fac076d31 100644
--- 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 *)