From: Claudio Sacerdoti Coen 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/?a=commitdiff_plain;h=4539aee6408cdc8efdfc981138c280c2dac79202;p=helm.git 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)