1. reset of statuses simplified

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

diff --git a/matita/matita/matita.ml b/matita/matita/matita.ml
index 94a34570aa7b8607941a6b83d950ae44147b4ccc..fa664e95b6a06ee2944557bd4688337bb214c09a 100644 (file)
--- a/matita/matita/matita.ml
+++ b/matita/matita/matita.ml
@@ -67,7 +67,7 @@ let init_debugging_menu gui =
       ignore (GMenu.separator_item ~packing:gui#main#debugMenu_menu#append ())
     in
     addDebugItem "dump aliases" (fun _ ->
-      let status = (MatitaScript.current ())#grafite_status in
+      let status = (MatitaScript.current ())#status in
       GrafiteDisambiguate.dump_aliases prerr_endline "" status);
 (* FG: DEBUGGING   
     addDebugItem "dump interpretations" (fun _ ->