From cb25e0f32f7581e1a49d1d1c109108763dfb882c Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Mon, 20 Apr 2009 02:26:10 +0000 Subject: [PATCH] Bug fixed: variable capture in previous commit prevented all aliases insertion. --- helm/software/matita/matitaEngine.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/helm/software/matita/matitaEngine.ml b/helm/software/matita/matitaEngine.ml index 75c3ebafc..5468c863a 100644 --- a/helm/software/matita/matitaEngine.ml +++ b/helm/software/matita/matitaEngine.ml @@ -81,7 +81,7 @@ let eval_ast ?do_heavy_checks lexicon_status ~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 @@ -90,7 +90,7 @@ let eval_ast ?do_heavy_checks lexicon_status | 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 = -- 2.39.2