X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_unification%2FcoercDb.ml;h=969d482c1601de65c62355fda02ed77afc1afb87;hb=8b55faddb06e3c4b0a13839210bb49170939b33e;hp=e636f87596a8e9e86729bc2c5e0c99e072151b21;hpb=e01614ddeb9a35e6203c0e0a93d304f80cb52893;p=helm.git

diff --git a/helm/ocaml/cic_unification/coercDb.ml b/helm/ocaml/cic_unification/coercDb.ml
index e636f8759..969d482c1 100644
--- a/helm/ocaml/cic_unification/coercDb.ml
+++ b/helm/ocaml/cic_unification/coercDb.ml
@@ -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