-let disambiguate_tactic text prefix_len 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) (Some goal)
- tac
- in
- GrafiteTypes.set_metasenv metasenv grafite_status,tac
-
-let disambiguate_command lexicon_status_ref grafite_status cmd =
- let baseuri = grafite_status#baseuri in
- let lexicon_status,metasenv,cmd =
- GrafiteDisambiguate.disambiguate_command ~baseuri
- !lexicon_status_ref (GrafiteTypes.get_proof_metasenv grafite_status) cmd
- in
- lexicon_status_ref := lexicon_status;
- GrafiteTypes.set_metasenv metasenv grafite_status,cmd
-
-let disambiguate_macro lexicon_status_ref grafite_status macro context =
- let metasenv,macro =
- GrafiteDisambiguate.disambiguate_macro
- lexicon_status_ref
- (GrafiteTypes.get_proof_metasenv grafite_status)
- context macro
- in
- GrafiteTypes.set_metasenv metasenv grafite_status,macro
-