X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=inline;f=helm%2Fsoftware%2Fmatita%2FmatitaScript.ml;h=0234c4824673837682dae785401920ab7abcd0ad;hb=eb9ca860db8cb06083765f7698179f16dee5303e;hp=a92b5b789707020df7c05b9de48ed906693cfe66;hpb=aa5f71baeba0299c0d29be01798f7a1ad13656f9;p=helm.git

diff --git a/helm/software/matita/matitaScript.ml b/helm/software/matita/matitaScript.ml
index a92b5b789..0234c4824 100644
--- a/helm/software/matita/matitaScript.ml
+++ b/helm/software/matita/matitaScript.ml
@@ -118,23 +118,14 @@ let wrap_with_make include_paths (f : GrafiteParser.statement) x =
           HLog.error "please create it.";
           raise (Failure ("No root file for "^mafilename))
       in
-      let initial_lexicon_status = 
-        CicNotation2.load_notation ~include_paths:[] BuildTimeConf.core_notation_script 
-      in
-      let b,x = 
+      let b = 
         try
           GrafiteSync.push ();
-          LexiconSync.time_travel ~present:x ~past:initial_lexicon_status;
+          LexiconSync.push ();
           let rc = MatitacLib.Make.make root [tgt] in 
+          LexiconSync.pop ();
           GrafiteSync.pop ();
-          CicNotation.reset ();
-          ignore(CicNotation2.load_notation ~include_paths:[]
-            BuildTimeConf.core_notation_script);
-          let x = List.fold_left (fun s c -> LexiconEngine.eval_command s c)
-            initial_lexicon_status (List.rev
-            x.LexiconEngine.lexicon_content_rev) 
-          in
-          rc,x
+          rc
         with 
         | exn ->
             HLog.error ("Unexpected " ^ snd(MatitaExcPp.to_string exn));