ocaml 3.09 transition

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

diff --git a/helm/coq-contribs/LAMBDA-TYPES/subst1_defs.v b/helm/coq-contribs/LAMBDA-TYPES/subst1_defs.v
index d1e0913481b31623c7ae65400644a5bde86e66dd..93e0d2ecff7729b4d8a85ec68d8be19ed4dfa702 100644 (file)
--- a/helm/coq-contribs/LAMBDA-TYPES/subst1_defs.v
+++ b/helm/coq-contribs/LAMBDA-TYPES/subst1_defs.v
@@ -32,8 +32,8 @@ Require Export subst0_defs.
       Try Subst0GenBase; XAuto.
       Qed.
 
-      Theorem subst1_gen_bref : (v,x:?; i,n:?) (subst1 i v (TBRef n) x) ->
-                                x = (TBRef n) \/
+      Theorem subst1_gen_lref : (v,x:?; i,n:?) (subst1 i v (TLRef n) x) ->
+                                x = (TLRef n) \/
                                 n = i /\ x = (lift (S n) (0) v).
       Intros; XElim H; Clear x; Intros;
       Try Subst0GenBase; XAuto.