-type cic_term = NCic.conjecture (* name, context, term *)
-let ctx_of (_,c,_) = c ;;
-
-let relocate status destination (name,source,t as orig) =
- if source == destination then status, orig else
- let u, d, metasenv, subst, o = status.pstatus 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 db = NCicUnifHint.db () in (* XXX fixme *)
- let (metasenv, subst), t =
- NCicMetaSubst.delift
- ~unify:(fun m s c t1 t2 ->
- try Some (NCicUnification.unify db m s c t1 t2)
- with
- | NCicUnification.UnificationFailure _
- | NCicUnification.Uncertain _ -> None)
- metasenv subst source 0 lc t
- in
- let status = { status with pstatus = u, d, metasenv, subst, o } in
- status, (name, destination, t)