From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Tue, 5 Feb 2013 13:16:22 +0000 (+0000)
Subject: Bug fixed: .ml/.mli files were opened/closed even when ocaml extraction was
X-Git-Tag: make_still_working~1271
X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=4539aee6408cdc8efdfc981138c280c2dac79202

Bug fixed: .ml/.mli files were opened/closed even when ocaml extraction was
not active.
---

diff --git a/matita/matita/matitaEngine.ml b/matita/matita/matitaEngine.ml
index a8e47b562..06b0da338 100644
--- a/matita/matita/matitaEngine.ml
+++ b/matita/matita/matitaEngine.ml
@@ -246,7 +246,7 @@ and compile ~compiling ~asserted ~include_paths fname =
   let status,ocamlfname =
    Common.modname_of_filename status false ocamlfname in
   let ocamlfname = ocamldirname ^ "/" ^ ocamlfname ^ ".ml" in
-  let status = OcamlExtractionTable.open_file status ~baseuri ocamlfname in
+  let status = OcamlExtraction.open_file status ~baseuri ocamlfname in
   let big_bang = Unix.gettimeofday () in
   let { Unix.tms_utime = big_bang_u ; Unix.tms_stime = big_bang_s} = 
     Unix.times () 
@@ -288,7 +288,7 @@ and compile ~compiling ~asserted ~include_paths fname =
     in
     let asserted, status =
      eval_from_stream ~compiling ~asserted ~include_paths status buf print_cb in
-    let status = OcamlExtractionTable.close_file status in
+    let status = OcamlExtraction.close_file status in
     let elapsed = Unix.time () -. time in
      (if Helm_registry.get_bool "matita.moo" then begin
        GrafiteTypes.Serializer.serialize ~baseuri:(NUri.uri_of_string baseuri)