X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2FmatitaGui.ml;h=13db5d2760a36216344c84676041cbad71b0b960;hb=a675ecc0a27920e2ce7d7058506f259a5c06dede;hp=a42500bd6bf16fd524efa2906d38f5cb18dd4a5f;hpb=cd664aefb80554952ed9b010f0c5199ce3a6f8f2;p=helm.git

diff --git a/matita/matita/matitaGui.ml b/matita/matita/matitaGui.ml
index a42500bd6..13db5d276 100644
--- a/matita/matita/matitaGui.ml
+++ b/matita/matita/matitaGui.ml
@@ -76,7 +76,7 @@ let save_moo grafite_status =
   | true, _ -> ()
   | _, true ->
      GrafiteTypes.Serializer.serialize ~baseuri:(NUri.uri_of_string baseuri)
-      grafite_status#dump
+      ~dependencies:grafite_status#dependencies grafite_status#dump
   | _ -> clean_current_baseuri grafite_status 
 ;;
     
@@ -859,7 +859,7 @@ class gui () =
            s#set_grafite_status status*)
          );
       MatitaGtkMisc.toggle_callback ~check:main#hideCoercionsMenuItem
-        ~callback:(fun enabled -> NTermCicContent.hide_coercions := enabled);
+        ~callback:(fun enabled -> Interpretations.hide_coercions := enabled);
       MatitaGtkMisc.toggle_callback ~check:main#unicodeAsTexMenuItem
         ~callback:(fun enabled ->
           Helm_registry.set_bool "matita.paste_unicode_as_tex" enabled);