+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
+ | _ -> []