From fbe9ce0580aa8248b839b8512f822d617514091b Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 13 Oct 2009 11:13:46 +0000 Subject: [PATCH] relocate fixed --- .../components/ng_tactics/nTacStatus.ml | 25 ++++++++----------- 1 file changed, 11 insertions(+), 14 deletions(-) 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)))); -- 2.39.2