+let relocate status destination (name,source,t as orig) =
+ if source == destination then status, orig else
+ let u, d, metasenv, subst, o = status#obj 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)
+ else
+ HExtlib.mk_list (NCic.Appl
+ [NCic.Sort NCic.Prop; NCic.Sort NCic.Prop]) 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)
+ else
+ HExtlib.mk_list (NCic.Appl
+ [NCic.Sort NCic.Prop; NCic.Sort NCic.Prop]) 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)
+ else
+ HExtlib.mk_list (NCic.Appl
+ [NCic.Sort NCic.Prop; NCic.Sort NCic.Prop]) j
+ | (n1, NCic.Decl _)::cl1, (n2, NCic.Def _)::cl2 -> assert false
+ | _::_, [] ->
+ HExtlib.mk_list (NCic.Appl
+ [NCic.Sort NCic.Prop; NCic.Sort NCic.Prop]) j
+ | _ -> []
+ in
+ let 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 (metasenv, subst), t =
+ NCicMetaSubst.delift
+ ~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 source 0 lc t