Debugging code commented out.

diff --git a/helm/ocaml/cic_unification/cicRefine.ml b/helm/ocaml/cic_unification/cicRefine.ml
index 202fa8cd798d3495a544f581128f2d510303c231..d3a297d43e88b517cec0e9caf4eef32e322896d9 100644 (file)
--- 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 ->