hgdome no longer used (RIP)

[helm.git] / matita / matita / matitaGui.ml

diff --git a/matita/matita/matitaGui.ml b/matita/matita/matitaGui.ml
index 417a758b7b5d088c5c59f224e4741e418365bba8..a0d731377cf65e6461963f654bf88801c41d948b 100644 (file)
--- a/matita/matita/matitaGui.ml
+++ b/matita/matita/matitaGui.ml
@@ -72,12 +72,9 @@ let clean_current_baseuri grafite_status =
 let save_moo grafite_status = 
   let script = MatitaScript.current () in
   let baseuri = grafite_status#baseuri in
-  let no_pstatus = 
-    grafite_status#proof_status = GrafiteTypes.No_proof 
-  in
-  match script#bos, script#eos, no_pstatus with
-  | true, _, _ -> ()
-  | _, true, true ->
+  match script#bos, script#eos with
+  | true, _ -> ()
+  | _, true ->
      let moo_fname = 
        LibraryMisc.obj_file_of_baseuri ~must_exist:false ~baseuri
         ~writable:true in
@@ -870,7 +867,7 @@ class gui () =
           | false ->
               CicNotation.set_active_notations []);
       MatitaGtkMisc.toggle_callback ~check:main#hideCoercionsMenuItem
-        ~callback:(fun enabled -> Acic2content.hide_coercions := enabled);
+        ~callback:(fun enabled -> NTermCicContent.hide_coercions := enabled);
       MatitaGtkMisc.toggle_callback ~check:main#unicodeAsTexMenuItem
         ~callback:(fun enabled ->
           Helm_registry.set_bool "matita.paste_unicode_as_tex" enabled);