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

[helm.git] / matita / components / ng_tactics / nTacStatus.ml

diff --git a/matita/components/ng_tactics/nTacStatus.ml b/matita/components/ng_tactics/nTacStatus.ml
index 9a6358baaf3e98ee5d4de13bd12e3ee9c02e2e61..143aac98e6294e9e35825bf9450e5a5fab8f4ba0 100644 (file)
--- a/matita/components/ng_tactics/nTacStatus.ml
+++ b/matita/components/ng_tactics/nTacStatus.ml
@@ -157,7 +157,7 @@ let relocate status destination (source,t as orig) =
             let u, d, metasenv, subst, o = status#obj in
             pp(lazy("delifting as " ^ 
               status#ppterm ~metasenv ~subst ~context:source 
-               (NCic.Meta (0,lc))));
+               (NCic.Meta (-1,lc))));
             let (metasenv, subst), t =
               NCicMetaSubst.delift status
                  ~unify:(fun m s c t1 t2 -> 
@@ -165,7 +165,7 @@ let relocate status destination (source,t as orig) =
                    with 
                     | NCicUnification.UnificationFailure _ 
                     | NCicUnification.Uncertain _ -> None) 
-               metasenv subst source 0 lc t
+               metasenv subst source (-1) lc t
             in
             let status = status#set_obj (u, d, metasenv, subst, o) in
             status, (ctx,t))