From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Tue, 22 Nov 2005 09:52:32 +0000 (+0000)
Subject: Debugging code commented out.
X-Git-Tag: V_0_7_2_3~6
X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=081cb0ae54c7e5babdedeea7559d667183a38638

Debugging code commented out.
---

diff --git a/helm/ocaml/cic_unification/cicRefine.ml b/helm/ocaml/cic_unification/cicRefine.ml
index 202fa8cd7..d3a297d43 100644
--- a/helm/ocaml/cic_unification/cicRefine.ml
+++ b/helm/ocaml/cic_unification/cicRefine.ml
@@ -1116,15 +1116,16 @@ and type_of_aux' metasenv context t ugraph =
                        match coer with
                        | CoercGraph.NoCoercion 
                        | CoercGraph.NotHandled _ ->
-                          let msg =
+                          let msg e =
                            lazy ("The term " ^
                             CicMetaSubst.ppterm_in_context subst hete
                              context ^ " has type " ^
                             CicMetaSubst.ppterm_in_context subst hety
                              context ^ " but is here used with type " ^
-                            CicMetaSubst.ppterm_in_context subst s context)
+                            CicMetaSubst.ppterm_in_context subst s context
+                             (* "\nReason: " ^ Lazy.force e*))
                           in
-                           enrich (fun _ -> msg) exn
+                           enrich msg exn
                        | CoercGraph.NotMetaClosed -> 
                            raise (Uncertain (lazy "Coercions on meta"))
                        | CoercGraph.SomeCoercion c ->