| GrafiteTypes.ProofMode s ->
{ grafite_status with GrafiteTypes.ng_status =
GrafiteTypes.ProofMode
- { s with NTactics.istatus = { s.NTactics.istatus with NTactics.lstatus = lexicon_status }}}
+ { s with NTacStatus.istatus = { s.NTacStatus.istatus with NTacStatus.lstatus = lexicon_status }}}
in
let new_grafite_status,new_objs =
GrafiteEngine.eval_ast
~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 =
+ let new_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.NTactics.istatus.NTactics.lstatus
+ | GrafiteTypes.ProofMode s -> s.NTacStatus.istatus.NTacStatus.lstatus
in
let new_lexicon_status =
- LexiconSync.add_aliases_for_objs lexicon_status new_objs in
+ LexiconSync.add_aliases_for_objs new_lexicon_status new_objs in
let new_aliases =
LexiconSync.alias_diff ~from:lexicon_status new_lexicon_status in
let _,intermediate_states =