ocaml 3.09 transition

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

diff --git a/helm/coq-contribs/LAMBDA-TYPES/pr0_lift.v b/helm/coq-contribs/LAMBDA-TYPES/pr0_lift.v
index f3dc1c5184dde691ed7b6a338a871a2d653da410..b6d9ba247c821442afc65f059ff42353e6816f57 100644 (file)
--- a/helm/coq-contribs/LAMBDA-TYPES/pr0_lift.v
+++ b/helm/coq-contribs/LAMBDA-TYPES/pr0_lift.v
@@ -2,9 +2,11 @@ Require lift_props.
 Require subst0_lift.
 Require pr0_defs.
 
-(*#* #caption "main properties of predicate \\texttt{pr0}" *)
+(*#* #caption "main properties of the relation $\\PrZ{}{}$" *)
 (*#* #clauses pr0_props *)
 
+(*#* #stop file *)
+
    Section pr0_lift. (*******************************************************)
 
 (*#* #caption "conguence with lift" *)
@@ -13,8 +15,6 @@ Require pr0_defs.
       Theorem pr0_lift: (t1,t2:?) (pr0 t1 t2) ->
                         (h,d:?) (pr0 (lift h d t1) (lift h d t2)).
 
-(*#* #stop file *)
-
       Intros until 1; XElim H; Intros.
 (* case 1: pr0_refl *)
       XAuto.
@@ -22,7 +22,7 @@ Require pr0_defs.
       LiftTailRw; XAuto.
 (* case 3 : pr0_beta *)
       LiftTailRw; XAuto.
-(* case 4: pr0_gamma *)
+(* case 4: pr0_upsilon *)
       LiftTailRw; Simpl; Arith0 d; Rewrite lift_d; XAuto.
 (* case 5: pr0_delta *)
       LiftTailRw; Simpl.