+(*
+
+type cic_term = NCic.conjecture
+type ast_term = string * int * CicNotationPt.term
+type position = Ctx of NCic.context | Term of cic_term
+
+let relocate (name,ctx,t as term) context =
+ if ctx = context then term else assert false
+;;
+
+let disambiguate (status : lowtac_status) (t : ast_term)
+ (ty : cic_term option) (where : position) =
+ let uri,height,metasenv,subst,obj = status.pstatus in
+ let context = match where with Ctx c -> c | Term (_,c,_) -> c in
+ let expty =
+ match ty with
+ | None -> None | Some ty -> let _,_,x = relocate ty context in Some x
+ in
+ let metasenv, subst, lexicon_status, t =
+ GrafiteDisambiguate.disambiguate_nterm expty
+ status.lstatus context metasenv subst t
+ in
+ let new_pstatus = uri,height,metasenv,subst,obj in
+ { lstatus = lexicon_status; pstatus = new_pstatus }, (None, context, t)
+;;
+
+let get_goal (status : lowtac_status) (g : int) =
+ let _,_,metasenv,_,_ = status.pstatus in
+ List.assoc g metasenv
+;;
+
+let return ~orig status =
+ let _,_,past,_,_ = orig.pstatus in
+ let _,_,present,_,_ = status.pstatus in
+ let open_goals, closed_goals = compare_menv ~past ~present in
+ status, open_goals, closed_goals
+;;
+
+let instantiate status i t =
+ let name,height,metasenv,subst,obj = status.pstatus in
+ let _, context, ty = List.assoc i metasenv in
+ let _,_,t = relocate t context in
+ let m = NCic.Meta (i,(0,NCic.Irl (List.length context))) in
+ let db = NCicUnifHint.db () in (* XXX fixme *)
+ let metasenv, subst = NCicUnification.unify db metasenv subst context m t in
+ { status with pstatus = (name,height,metasenv,subst,obj) }
+;;
+
+let apply t (status as orig, goal) =
+ let goalty = get_goal status goal in
+ let status, t = disambiguate status t (Some goalty) (Term goalty) in
+ let status = instantiate status goal t in
+ return ~orig status