X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_unification%2FcicRefine.ml;h=d3a297d43e88b517cec0e9caf4eef32e322896d9;hb=97c2d258a5c524eb5c4b85208899d80751a2c82f;hp=202fa8cd798d3495a544f581128f2d510303c231;hpb=b0ee377b3d84305cd121bf8495c02ac3adfa85cc;p=helm.git

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