From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Thu, 9 Jun 2005 11:46:58 +0000 (+0000)
Subject: added debug item for coercion
X-Git-Tag: PRE_INDEX_1~14
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=2ba4fdc5cd4af9719fb3286a41a4480aa8b0d48b;p=helm.git

added debug item for coercion
---

diff --git a/helm/matita/matita.ml b/helm/matita/matita.ml
index d0959e453..97595d192 100644
--- a/helm/matita/matita.ml
+++ b/helm/matita/matita.ml
@@ -142,6 +142,14 @@ let _ =
       (fun _ ->
          if script#onGoingProof () then
            MatitaLog.debug (CicMetaSubst.ppmetasenv script#proofMetasenv []));
+    addDebugItem "dump coercions Db" (fun _ ->
+      List.iter (
+        fun (s,t,u) -> 
+          MatitaLog.debug (
+            UriManager.name_of_uri u ^ ":" ^ 
+            UriManager.name_of_uri s ^ " -> " ^ UriManager.name_of_uri t))
+      (CoercDb.to_list ())
+    );
     addDebugItem "rotate light bulbs"
       (fun _ ->
          let nb = gui#main#hintNotebook in