ocaml 3.09 transition

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

diff --git a/helm/coq-contribs/LAMBDA-TYPES/lift_tlt.v b/helm/coq-contribs/LAMBDA-TYPES/lift_tlt.v
index 3a9cb3fce0b71562e594c5cc0769860ac2286184..7319f3264e91db6456f0c9491f8f725d2c99389f 100644 (file)
--- a/helm/coq-contribs/LAMBDA-TYPES/lift_tlt.v
+++ b/helm/coq-contribs/LAMBDA-TYPES/lift_tlt.v
@@ -17,12 +17,12 @@ Require lift_defs.
       XElim t; Intros.
 (* case 1: TSort *)
       XAuto.
-(* case 2: TBRef n *)
+(* case 2: TLRef n *)
       Apply (lt_le_e n d); Intros.
 (* case 2.1: n < d *)
-      Rewrite lift_bref_lt; XAuto.
+      Rewrite lift_lref_lt; XAuto.
 (* case 2.2: n >= d *)
-      Rewrite lift_bref_ge; [ Simpl | XAuto ].
+      Rewrite lift_lref_ge; [ Simpl | XAuto ].
       Rewrite (H n); XAuto.
 (* case 3: TTail k *)
       XElim k; Intros; LiftTailRw; Simpl.
@@ -48,12 +48,12 @@ Require lift_defs.
       XElim t; Intros.
 (* case 1: TSort *)
       XAuto.
-(* case 2: TBRef *)
+(* case 2: TLRef *)
       Apply (lt_le_e n d); Intros.
 (* case 2.1: n < d *)
-      Repeat Rewrite lift_bref_lt; Simpl; XAuto.
+      Repeat Rewrite lift_lref_lt; Simpl; XAuto.
 (* case 2.2: n >= d *)
-      Repeat Rewrite lift_bref_ge; Simpl; Try Rewrite <- plus_n_Sm; XAuto.
+      Repeat Rewrite lift_lref_ge; Simpl; Try Rewrite <- plus_n_Sm; XAuto.
 (* case 3: TTail k *)
       XElim k; Intros; LiftTailRw; Simpl.
 (* case 1 : bind b *)
@@ -84,6 +84,4 @@ Require lift_defs.
 
       Hints Resolve lift_tlt_dx : ltlc.
 
-(*#* #start file *)
-
 (*#* #single *)