+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 : low_status) (g : int) =
+ let _,_,metasenv,_,_ = status.pstatus in
+ List.assoc goal 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 apply t (status as orig,goal) =
+ let goal = get_goal status goal in
+ let status, t = disambiguate status t goal (Term goal) in
+ let subst, metasenv =
+ (goal, (name, context, t, gty)):: subst,
+ List.filter(fun (x,_) -> x <> goal) metasenv
+ in
+ return ~orig status
+;;
+
+*)
+
+