let disambiguate_macro_term term status user_goal =
let module MD = MatitaDisambiguator in
let dbd = MatitaDb.instance () in
- let metasenv = MatitaMisc.get_proof_metasenv status in
- let context = MatitaMisc.get_proof_context status user_goal in
+ let metasenv = MatitaTypes.get_proof_metasenv status in
+ let context = MatitaTypes.get_proof_context status user_goal in
let interps =
MD.disambiguate_term ~dbd ~context ~metasenv ~aliases:status.aliases
~universe:(Some status.multi_aliases) term in
[], parsed_text_length
(* REAL macro *)
| TA.Hint loc ->
- let proof = MatitaMisc.get_current_proof status in
+ let proof = MatitaTypes.get_current_proof status in
let proof_status = proof, user_goal in
let l = List.map fst (MQ.experimental_hint ~dbd proof_status) in
let selected = guistuff.urichooser l in
) selected;
assert false)
| TA.Check (_,term) ->
- let metasenv = MatitaMisc.get_proof_metasenv status in
- let context = MatitaMisc.get_proof_context status user_goal in
+ let metasenv = MatitaTypes.get_proof_metasenv status in
+ let context = MatitaTypes.get_proof_context status user_goal in
let interps =
MatitaDisambiguator.disambiguate_term ~dbd ~context ~metasenv
~aliases:status.aliases ~universe:(Some status.multi_aliases) term
| Incomplete_proof _ -> true
| Intermediate _ -> assert false
-(* method proofStatus = MatitaMisc.get_proof_status self#status *)
- method proofMetasenv = MatitaMisc.get_proof_metasenv self#status
- method proofContext = MatitaMisc.get_proof_context self#status userGoal
- method proofConclusion = MatitaMisc.get_proof_conclusion self#status userGoal
- method stack = MatitaMisc.get_stack self#status
+(* method proofStatus = MatitaTypes.get_proof_status self#status *)
+ method proofMetasenv = MatitaTypes.get_proof_metasenv self#status
+ method proofContext = MatitaTypes.get_proof_context self#status userGoal
+ method proofConclusion = MatitaTypes.get_proof_conclusion self#status userGoal
+ method stack = MatitaTypes.get_stack self#status
method setGoal n = userGoal <- n
method goal = userGoal