+let disambiguate_command lexicon_status_ref status cmd =
+ let lexicon_status,metasenv,cmd =
+ GrafiteDisambiguate.disambiguate_command
+ ~baseuri:(
+ try
+ Some (GrafiteTypes.get_string_option status "baseuri")
+ with
+ GrafiteTypes.Option_error _ -> None)
+ !lexicon_status_ref (GrafiteTypes.get_proof_metasenv status) cmd
+ in
+ lexicon_status_ref := lexicon_status;
+ GrafiteTypes.set_metasenv metasenv status,cmd
+
+let disambiguate_tactic lexicon_status_ref status goal tac =
+ let metasenv,tac =
+ GrafiteDisambiguate.disambiguate_tactic
+ lexicon_status_ref
+ (GrafiteTypes.get_proof_context status goal)
+ (GrafiteTypes.get_proof_metasenv status)
+ tac
+ in
+ GrafiteTypes.set_metasenv metasenv status,tac
+
+let eval_ast ?do_heavy_checks ?clean_baseuri lexicon_status
+ status ast