+let disambiguate_tactic lexicon_status_ref grafite_status goal tac =
+ let metasenv,tac =
+ GrafiteDisambiguate.disambiguate_tactic
+ lexicon_status_ref
+ (GrafiteTypes.get_proof_context grafite_status goal)
+ (GrafiteTypes.get_proof_metasenv grafite_status)
+ tac
+ in
+ GrafiteTypes.set_metasenv metasenv grafite_status,tac
+
+let disambiguate_command lexicon_status_ref grafite_status cmd =