- content/interpretations.ml and ng_cic_content/nTermCicContent.ml where

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

diff --git a/matita/matita/matitaGui.ml b/matita/matita/matitaGui.ml
index a42500bd6bf16fd524efa2906d38f5cb18dd4a5f..d963cf6a27d7251103f0bb9f9509d717c0dcd7d8 100644 (file)
--- a/matita/matita/matitaGui.ml
+++ b/matita/matita/matitaGui.ml
@@ -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);