]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/cic_unification/coercDb.ml
Every exception that used to have type string is now a string Lazy.t.
[helm.git] / helm / ocaml / cic_unification / coercDb.ml
index e636f87596a8e9e86729bc2c5e0c99e072151b21..969d482c1601de65c62355fda02ed77afc1afb87 100644 (file)
@@ -24,7 +24,7 @@
  *)
 
 type coerc_carr = Uri of UriManager.uri | Sort of Cic.sort | Term of Cic.term
-exception EqCarrNotImplemented of string
+exception EqCarrNotImplemented of string Lazy.t
 exception EqCarrOnNonMetaClosed
 
 let db = ref []
@@ -48,8 +48,8 @@ let eq_carr src tgt =
     CicUtil.is_meta_closed t1 && CicUtil.is_meta_closed t2 -> 
       raise 
         (EqCarrNotImplemented 
-          ("Unsupported carr for coercions: " ^ 
-            CicPp.ppterm t1 ^ " or " ^ CicPp.ppterm t2))
+          (lazy ("Unsupported carr for coercions: " ^ 
+            CicPp.ppterm t1 ^ " or " ^ CicPp.ppterm t2)))
   | _ -> raise EqCarrOnNonMetaClosed
 
 let name_of_carr = function