New debug item to print aliases.

diff --git a/helm/software/matita/matita.ml b/helm/software/matita/matita.ml
index 62e425bf38b13dcb28fc0c7f7e7e553d97d113bb..64d1a4513ebed04a6c7fa8427aa8094a9f4b3da3 100644 (file)
--- a/helm/software/matita/matita.ml
+++ b/helm/software/matita/matita.ml
@@ -116,6 +116,9 @@ let _ =
     let addDebugSeparator () =
       ignore (GMenu.separator_item ~packing:gui#main#debugMenu_menu#append ())
     in
+    addDebugItem "dump aliases" (fun _ ->
+      let status = script#lexicon_status in
+      HLog.debug (DisambiguatePp.pp_environment status.LexiconEngine.aliases));
     addDebugItem "dump environment to \"env.dump\"" (fun _ ->
       let oc = open_out "env.dump" in
       CicEnvironment.dump_to_channel oc;