Bug fixed: no .moo can be generated if the status is <> No_proof

diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml
index 540a839ddd99fec4fc09f04b1ee82875aa395c2d..8e16be52cdb5a45cf4df39527b1ef6ef421fb618 100644 (file)
--- a/helm/matita/matitaGui.ml
+++ b/helm/matita/matitaGui.ml
@@ -67,9 +67,10 @@ let clean_current_baseuri status =
 
 let ask_and_save_moo_if_needed parent fname status = 
   let save () =
-    MatitacLib.dump_moo_to_file fname status.MatitaTypes.moo_content_rev
-  in
-  if (MatitaScript.instance ())#eos then
+    MatitacLib.dump_moo_to_file fname status.MatitaTypes.moo_content_rev in
+  if (MatitaScript.instance ())#eos &&
+     status.MatitaTypes.proof_status = MatitaTypes.No_proof
+  then
     begin
       let mooname = 
         MatitaMisc.obj_file_of_script fname