ocaml 3.09 transition

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

diff --git a/helm/coq-contribs/LAMBDA-TYPES/lift_defs.v b/helm/coq-contribs/LAMBDA-TYPES/lift_defs.v
index 1f61d9fadaf75afdc6ea79d20019d847953fb365..8b69ec4b49c62cb3c639e182bd8c8c3990b8f20a 100644 (file)
--- a/helm/coq-contribs/LAMBDA-TYPES/lift_defs.v
+++ b/helm/coq-contribs/LAMBDA-TYPES/lift_defs.v
@@ -183,7 +183,9 @@ Require Export terms_defs.
             | [ H1: (le ?1 ?2); H2: (lt ?2 (plus ?1 ?3));
                 H3: (TLRef ?2) = (lift ?3 ?1 ?4) |- ? ] ->
                Apply (lift_gen_lref_false ?3 ?1 ?2 H1 H2 ?4 H3); XAuto
-            | [ H: (TLRef ?1) = (lift (1) ?1 ?2) |- ? ] ->
+            | [ _: (TLRef ?1) = (lift (S ?1) (0) ?2) |- ? ] ->
+              EApply lift_gen_lref_false; [ Idtac | Idtac | XEAuto ]; XEAuto
+           | [ H: (TLRef ?1) = (lift (1) ?1 ?2) |- ? ] ->
                LApply (lift_gen_lref_false (1) ?1 ?1); [ Intros H_x | XAuto ];
                LApply H_x; [ Clear H_x; Intros H_x | Arith7' ?1; XAuto ];
                LApply (H_x ?2); [ Clear H_x; Intros H_x | XAuto ];