...

[helm.git] / helm / software / matita / matitaScript.ml

diff --git a/helm/software/matita/matitaScript.ml b/helm/software/matita/matitaScript.ml
index 0234c4824673837682dae785401920ab7abcd0ad..cbaa08721cca870b1643e5005cbf7a62ae4a6825 100644 (file)
--- a/helm/software/matita/matitaScript.ml
+++ b/helm/software/matita/matitaScript.ml
@@ -118,19 +118,7 @@ let wrap_with_make include_paths (f : GrafiteParser.statement) x =
           HLog.error "please create it.";
           raise (Failure ("No root file for "^mafilename))
       in
-      let b = 
-        try
-          GrafiteSync.push ();
-          LexiconSync.push ();
-          let rc = MatitacLib.Make.make root [tgt] in 
-          LexiconSync.pop ();
-          GrafiteSync.pop ();
-          rc
-        with 
-        | exn ->
-            HLog.error ("Unexpected " ^ snd(MatitaExcPp.to_string exn));
-            assert false
-      in
+      let b = MatitacLib.Make.make root [tgt] in
       if b then 
         try f ~include_paths x with LexiconEngine.IncludedFileNotCompiled _ ->
          raise