X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_unification%2FcoercGraph.ml;h=2e69c648657646867879bebbdafd49148ea7212c;hb=22ff3a49e742b4289c96d518479a8e08c9192b7c;hp=469e334a7358e0b7dcbb03ea32607690a0d32fe5;hpb=0245778d76e4d7656c1d8a05dc19738f1a953d68;p=helm.git

diff --git a/helm/ocaml/cic_unification/coercGraph.ml b/helm/ocaml/cic_unification/coercGraph.ml
index 469e334a7..2e69c6486 100644
--- a/helm/ocaml/cic_unification/coercGraph.ml
+++ b/helm/ocaml/cic_unification/coercGraph.ml
@@ -29,7 +29,7 @@ type coercion_search_result =
   | SomeCoercion of Cic.term
   | NoCoercion
   | NotMetaClosed
-  | NotHandled of string
+  | NotHandled of string Lazy.t
 
 let debug = false
 let debug_print s = if debug then prerr_endline (Lazy.force s) else ()
@@ -115,7 +115,7 @@ let generate_composite_closure c1 c2 univ =
       CicTypeChecker.type_of_aux' [] [] c univ
     with CicTypeChecker.TypeCheckerFailure s as exn ->
       debug_print (lazy (sprintf "Generated composite coercion:\n%s\n%s" 
-        (CicPp.ppterm c) s));
+        (CicPp.ppterm c) (Lazy.force s)));
       raise exn
   in
   let cleaned_ty =