ocaml 3.09 transition

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

diff --git a/helm/coq-contribs/LAMBDA-TYPES/pr3_confluence.v b/helm/coq-contribs/LAMBDA-TYPES/pr3_confluence.v
index 2267e88ae13d3ae62da2d7bc1b47b5936fc1e077..6f5019bc908e39a50cff7da1beba97af31809b27 100644 (file)
--- a/helm/coq-contribs/LAMBDA-TYPES/pr3_confluence.v
+++ b/helm/coq-contribs/LAMBDA-TYPES/pr3_confluence.v
@@ -3,24 +3,23 @@ Require pr3_defs.
 
    Section pr3_confluence. (*************************************************)
 
+(*#* #stop theorem *)
+
 (*#* #caption "confluence with single step reduction: strip lemma" *)
 (*#* #cap #cap c, t0, t1, t2, t *)
 
       Theorem pr3_strip : (c:?; t0,t1:?) (pr3 c t0 t1) -> (t2:?) (pr2 c t0 t2) ->
                           (EX t | (pr3 c t1 t) & (pr3 c t2 t)).
-
-(*#* #stop proof *)
-
       Intros until 1; XElim H; Intros.
-(* case 1 : pr3_r *)
+(* case 1 : pr3_refl *)
       XEAuto.
-(* case 2 : pr3_u *)
+(* case 2 : pr3_sing *)
       Pr2Confluence.
       LApply (H1 x); [ Clear H1 H2; Intros H1 | XAuto ].
       XElim H1; Intros; XEAuto.
       Qed.
 
-(*#* #start proof *)
+(*#* #start theorem *)
 
 (*#* #caption "confluence with itself: Church-Rosser property" *)
 (*#* #cap #cap c, t0, t1, t2, t *)
@@ -31,9 +30,9 @@ Require pr3_defs.
 (*#* #stop file *)
 
       Intros until 1; XElim H; Intros.
-(* case 1 : pr3_r *)
+(* case 1 : pr3_refl *)
       XEAuto.
-(* case 2 : pr3_u *)
+(* case 2 : pr3_sing *)
       LApply (pr3_strip c t3 t5); [ Clear H2; Intros H2 | XAuto ].
       LApply (H2 t2); [ Clear H H2; Intros H | XAuto ].
       XElim H; Intros.