]> matita.cs.unibo.it Git - helm.git/commitdiff
CicExportation branched. Change "if false" with "if true" to activate automatic
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Sun, 4 Nov 2007 17:26:29 +0000 (17:26 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Sun, 4 Nov 2007 17:26:29 +0000 (17:26 +0000)
exportation of OCaml files during compilation.

matita/matitacLib.ml

index c2cdd7ef5787e886f9629ca8bb5bb7bf27677bf4..1da706749fa1194de8e3625dfb91c75c7668d035 100644 (file)
@@ -304,6 +304,13 @@ let main ~mode =
   MatitaInit.initialize_all ();
   (* must be called after init since args are set by cmdline parsing *)
   let fname = fname () in
+  if false then
+   let basename = Filename.chop_extension fname in
+   let f = open_out (basename ^ ".ml") in
+    LibrarySync.set_object_declaration_hook
+     (fun _ obj ->
+       output_string f (CicExportation.ppobj basename obj);
+       flush f);
   let system_mode =  Helm_registry.get_bool "matita.system" in
   let bench_mode =  Helm_registry.get_bool "matita.bench" in
   if bench_mode then