ocaml 3.09 transition

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

diff --git a/helm/coq-contribs/LAMBDA-TYPES/subst0_tlt.v b/helm/coq-contribs/LAMBDA-TYPES/subst0_tlt.v
index 87bf9c8c087698af9164aee93d8d59438234a99c..b5fef207b6cbadb9c9d0a4e2e4fb04f42690cf82 100644 (file)
--- a/helm/coq-contribs/LAMBDA-TYPES/subst0_tlt.v
+++ b/helm/coq-contribs/LAMBDA-TYPES/subst0_tlt.v
@@ -11,7 +11,7 @@ Require subst0_defs.
                                  (lt (weight_map f (lift (S d) (0) u)) (g d)) ->
                                  (le (weight_map f z) (weight_map g t)).
       Intros until 1; XElim H.
-(* case 1: subst0_bref *)
+(* case 1: subst0_lref *)
       Intros; XAuto.
 (* case 2: subst0_fst *)
       XElim k; [ XElim b | Idtac ]; Simpl; [ Auto 7 with ltlc (**) | XAuto | XAuto | XAuto ].
@@ -26,7 +26,7 @@ Require subst0_defs.
                                  (lt (weight_map f (lift (S d) (0) u)) (g d)) ->
                                  (lt (weight_map f z) (weight_map g t)).
       Intros until 1; XElim H.
-(* case 1: subst0_bref *)
+(* case 1: subst0_lref *)
       Intros; XAuto.
 (* case 2: subst0_fst *)
       XElim k; [ XElim b | Idtac ]; Simpl; Intros;