X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_tactics%2FnTacStatus.ml;h=70ddfeaa9499eaccd55636cd0b366e2f719b4656;hb=fbe9ce0580aa8248b839b8512f822d617514091b;hp=f5a7c65ba73166329260334c2a2b200985473e95;hpb=d02e9de60490bc1928ca7d32db2263e21c0148de;p=helm.git

diff --git a/helm/software/components/ng_tactics/nTacStatus.ml b/helm/software/components/ng_tactics/nTacStatus.ml
index f5a7c65ba..70ddfeaa9 100644
--- a/helm/software/components/ng_tactics/nTacStatus.ml
+++ b/helm/software/components/ng_tactics/nTacStatus.ml
@@ -74,39 +74,36 @@ let relocate status destination (source,t as orig) =
  let rc = 
    if source == destination then status, orig else
     let u, d, metasenv, subst, o = status#obj in
-    let hole = NCic.Sort NCic.Prop in 
-    (* XXX (Prop Prop) is so illtyped that
-           even the trie used for hints lookup complains. We say Prop. 
-    *)
+    let cons x (a,b) = a, x::b in
     let rec lcp ctx j i = function
       | (n1, NCic.Decl t1 as e)::cl1, (n2, NCic.Decl t2)::cl2 ->
           if n1 = n2 && 
              NCicReduction.are_convertible ctx ~subst ~metasenv t1 t2 then
-            NCic.Rel i :: lcp (e::ctx)(j-1) (i-1) (cl1,cl2)
+            cons (NCic.Rel i) (lcp (e::ctx)(j-1) (i-1) (cl1,cl2))
           else
-            HExtlib.mk_list hole j
+            j, []
       | (n1, NCic.Def (b1,t1) as e)::cl1, (n2, NCic.Def (b2,t2))::cl2 ->
           if n1 = n2 && 
              NCicReduction.are_convertible ctx ~subst ~metasenv t1 t2 &&
              NCicReduction.are_convertible ctx ~subst ~metasenv b1 b2 then
-            NCic.Rel i :: lcp (e::ctx)(j-1) (i-1) (cl1,cl2)
+            cons (NCic.Rel i) (lcp (e::ctx)(j-1) (i-1) (cl1,cl2))
           else
-            HExtlib.mk_list hole j
+            j, []
       | (n1, NCic.Def (b1,t1) as e)::cl1, (n2, NCic.Decl t2)::cl2 ->
           if n1 = n2 && 
              NCicReduction.are_convertible ctx ~subst ~metasenv t1 t2 then
-            NCic.Rel i :: lcp (e::ctx)(j-1) (i-1) (cl1,cl2)
+            cons (NCic.Rel i) (lcp (e::ctx)(j-1) (i-1) (cl1,cl2))
           else
-            HExtlib.mk_list hole j
+            j, []
       | (n1, NCic.Decl _)::cl1, (n2, NCic.Def _)::cl2 -> assert false
-      | _::_, [] -> HExtlib.mk_list hole j
-      | _ -> []
+      | _::_, [] -> j, []
+      | _ -> 0, []
     in
-    let lc = 
+    let shift, lc = 
       lcp [] (List.length destination) (List.length source) 
         (List.rev destination, List.rev source)
     in
-    let lc = (0,NCic.Ctx (List.rev lc)) in
+    let lc = (shift,NCic.Ctx (List.rev lc)) in
     pp(lazy("delifting as " ^ 
       NCicPp.ppterm ~metasenv ~subst ~context:source 
        (NCic.Meta (0,lc))));