From f75a636a0f3d548bcf485df9b51ac72ed4759c97 Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Sat, 23 Aug 2008 19:10:31 +0000
Subject: [PATCH] New debug item to print aliases.

---
 helm/software/matita/matita.ml | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/helm/software/matita/matita.ml b/helm/software/matita/matita.ml
index 62e425bf3..64d1a4513 100644
--- 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;
-- 
2.39.2