Delift used to produce not well typed substitutions. In turn, this

[helm.git] / matita / components / ng_refiner / nCicUnification.ml

diff --git a/matita/components/ng_refiner/nCicUnification.ml b/matita/components/ng_refiner/nCicUnification.ml
index c8f67f1769e523fd53df6f7c067d99c68bcfa915..064a5f6ad08a7c9c99c7933c26991e8a0f484a12 100644 (file)
--- a/matita/components/ng_refiner/nCicUnification.ml
+++ b/matita/components/ng_refiner/nCicUnification.ml
@@ -913,7 +913,7 @@ and delift_type_wrt_terms status metasenv subst context t args =
            with UnificationFailure _ | Uncertain _ -> None
          in
          indent := ind; res)
-      metasenv subst context 0 (0,NCic.Ctx lc) t
+      metasenv subst context (-1) (0,NCic.Ctx lc) t
    with
       NCicMetaSubst.MetaSubstFailure _
     | NCicMetaSubst.Uncertain _ -> (metasenv, subst), t