]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/cic_unification/coercGraph.ml
Every exception that used to have type string is now a string Lazy.t.
[helm.git] / helm / ocaml / cic_unification / coercGraph.ml
index 469e334a7358e0b7dcbb03ea32607690a0d32fe5..2e69c648657646867879bebbdafd49148ea7212c 100644 (file)
@@ -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 =