| 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
;;
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);