lexicon_status_ref := lexicon_status;
GrafiteTypes.set_metasenv metasenv grafite_status,cmd
-let disambiguate_macro lexicon_status_ref grafite_status macro goal =
+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)
- (GrafiteTypes.get_proof_context grafite_status goal)
- macro
+ context macro
in
GrafiteTypes.set_metasenv metasenv grafite_status,macro