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