CicExportation branched. Change "if false" with "if true" to activate automatic

[helm.git] / matita / matitacLib.ml

diff --git a/matita/matitacLib.ml b/matita/matitacLib.ml
index c2cdd7ef5787e886f9629ca8bb5bb7bf27677bf4..1da706749fa1194de8e3625dfb91c75c7668d035 100644 (file)
--- a/matita/matitacLib.ml
+++ b/matita/matitacLib.ml
@@ -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