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

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

diff --git a/matita/components/ng_refiner/nCicRefiner.ml b/matita/components/ng_refiner/nCicRefiner.ml
index d26edf6d9d3bd40783963909cc84bd9dcaaa1d13..bb90cf7215ec0ed2bc85d94e6c22de69e65a4075 100644 (file)
--- a/matita/components/ng_refiner/nCicRefiner.ml
+++ b/matita/components/ng_refiner/nCicRefiner.ml
@@ -70,7 +70,7 @@ let exp_implicit status ~localise metasenv subst context with_type t =
               ~unify:(fun m s c t1 t2 ->
                 try Some (NCicUnification.unify status m s c t1 t2)
                 with NCicUnification.UnificationFailure _ | NCicUnification.Uncertain _ -> None)
-              metasenv subst context 0 (0,NCic.Irl 0) typ
+              metasenv subst context (-1) (0,NCic.Irl 0) typ
             with
               NCicMetaSubst.MetaSubstFailure _
             | NCicMetaSubst.Uncertain _ ->