From a7ed0b694086ba14b337c82b82f02f7be16c680f Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Fri, 5 Nov 2010 11:13:09 +0000 Subject: [PATCH] - recently introduced bug fixed: the new intermediate statuses for aliases used to already have all the aliases in them --- matita/matita/matitaEngine.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/matita/matita/matitaEngine.ml b/matita/matita/matitaEngine.ml index 4c246a253..429f75cd3 100644 --- a/matita/matita/matitaEngine.ml +++ b/matita/matita/matitaEngine.ml @@ -53,7 +53,7 @@ let eval_macro_screenshot (status : GrafiteTypes.status) name = let eval_ast ~include_paths ?do_heavy_checks status (text,prefix_len,ast) = let baseuri = status#baseuri in - let new_aliases,status = + let new_aliases,new_status = GrafiteDisambiguate.eval_with_new_aliases status (fun status -> GrafiteEngine.eval_ast ~include_paths ?do_heavy_checks status @@ -78,9 +78,9 @@ let eval_ast ~include_paths ?do_heavy_checks status (text,prefix_len,ast) = GrafiteAst.WithPreferences [k,value] in status, (status ,Some (k,value))::acc - ) (status,[]) new_aliases + ) (status,[]) new_aliases (* WARNING: this must be the old status! *) in - (status,None)::intermediate_states + (new_status,None)::intermediate_states ;; exception TryingToAdd of string -- 2.39.2