- ~disambiguate_tactic:(wrap (disambiguate_tactic text prefix_len lexicon_status_ref))
- ~disambiguate_command:(wrap (disambiguate_command lexicon_status_ref))
- ~disambiguate_macro:(wrap (disambiguate_macro lexicon_status_ref))
- ?do_heavy_checks grafite_status (text,prefix_len,ast) in
- let lexicon_status =
- if !changed_lexicon then
- !lexicon_status_ref
- else
- match new_grafite_status.GrafiteTypes.ng_status with
- | GrafiteTypes.CommandMode l -> l
- | GrafiteTypes.ProofMode s -> s.NTacStatus.istatus.NTacStatus.lstatus
+ ~disambiguate_tactic:(disambiguate_tactic text prefix_len lexicon_status_ref)
+ ~disambiguate_command:(disambiguate_command lexicon_status_ref)
+ ~disambiguate_macro:(disambiguate_macro lexicon_status_ref)
+ ?do_heavy_checks grafite_status (text,prefix_len,ast)