ocaml 3.09 transition

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

diff --git a/helm/coq-contribs/LAMBDA-TYPES/subst0_gen.v b/helm/coq-contribs/LAMBDA-TYPES/subst0_gen.v
index 7a0acfeb6cf803c6c93e48b0f65ae568f1343339..d46ca3555e1b1ee07432ef57719698293678d226 100644 (file)
--- a/helm/coq-contribs/LAMBDA-TYPES/subst0_gen.v
+++ b/helm/coq-contribs/LAMBDA-TYPES/subst0_gen.v
@@ -17,14 +17,14 @@ Require subst0_defs.
       XElim t1; Intros.
 (* case 1: TSort *)
       Rewrite lift_sort in H; Subst0GenBase.
-(* case 2: TBRef n *)
+(* case 2: TLRef n *)
       Apply (lt_le_e n (S (plus i d))); Intros.
 (* case 2.1: n < 1 + i + d *)
-      Rewrite lift_bref_lt in H; [ Idtac | XAuto ].
+      Rewrite lift_lref_lt in H; [ Idtac | XAuto ].
       Subst0GenBase; Rewrite H1; Rewrite H.
       Rewrite <- lift_d; Simpl; XEAuto.
 (* case 2.2: n >= 1 + i + d *)
-      Rewrite lift_bref_ge in H; [ Idtac | XAuto ].
+      Rewrite lift_lref_ge in H; [ Idtac | XAuto ].
       Subst0GenBase; Rewrite <- H in H0.
       EApply le_false; [ Idtac | Apply H0 ]; XAuto.
 (* case 3: TTail k *)
@@ -49,14 +49,14 @@ Require subst0_defs.
       XElim t; Intros.
 (* case 1: TSort *)
       Rewrite lift_sort in H1; Subst0GenBase.
-(* case 2: TBRef n *)
+(* case 2: TLRef n *)
       Apply (lt_le_e n d); Intros.
 (* case 2.1: n < d *)
-      Rewrite lift_bref_lt in H1; [ Idtac | XAuto ].
+      Rewrite lift_lref_lt in H1; [ Idtac | XAuto ].
       Subst0GenBase; Rewrite H1 in H2.
       EApply le_false; [ Apply H | XAuto ].
 (* case 2.2: n >= d *)
-      Rewrite lift_bref_ge in H1; [ Idtac | XAuto ].
+      Rewrite lift_lref_ge in H1; [ Idtac | XAuto ].
       Subst0GenBase; Rewrite <- H1 in H0.
       EApply le_false; [ Apply H2 | XEAuto ].
 (* case 3: TTail k *)
@@ -87,14 +87,14 @@ Require subst0_defs.
       XElim t1; Intros.
 (* case 1: TSort *)
       Rewrite lift_sort in H; Subst0GenBase.
-(* case 2: TBRef n *)
+(* case 2: TLRef n *)
       Apply (lt_le_e n d); Intros.
 (* case 2.1: n < d *)
-      Rewrite lift_bref_lt in H; [ Idtac | XAuto ].
+      Rewrite lift_lref_lt in H; [ Idtac | XAuto ].
       Subst0GenBase; Rewrite H in H1.
       EApply le_false; [ Apply H0 | XAuto ].
 (* case 2.2: n >= d *)
-      Rewrite lift_bref_ge in H; [ Idtac | XAuto ].
+      Rewrite lift_lref_ge in H; [ Idtac | XAuto ].
       Subst0GenBase; Rewrite <- H; Rewrite H2.
       Rewrite minus_plus_r.
       EApply ex2_intro; [ Idtac | XAuto ].