From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Fri, 5 Nov 2010 11:13:09 +0000 (+0000)
Subject: - recently introduced bug fixed: the new intermediate statuses for
X-Git-Tag: make_still_working~2718
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=a7ed0b694086ba14b337c82b82f02f7be16c680f;p=helm.git

- recently introduced bug fixed: the new intermediate statuses for
aliases used to already have all the aliases in them
---

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