GrafiteDisambiguate.disambiguate_tactic
lexicon_status_ref
(GrafiteTypes.get_proof_context grafite_status goal)
- (GrafiteTypes.get_proof_metasenv grafite_status)
+ (GrafiteTypes.get_proof_metasenv grafite_status) (Some goal)
tac
in
GrafiteTypes.set_metasenv metasenv grafite_status,tac