From 2ba4fdc5cd4af9719fb3286a41a4480aa8b0d48b Mon Sep 17 00:00:00 2001
From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Thu, 9 Jun 2005 11:46:58 +0000
Subject: [PATCH] added debug item for coercion

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

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
-- 
2.39.2