Every exception that used to have type string is now a string Lazy.t.

[helm.git] / helm / ocaml / cic_proof_checking / cicElim.ml

diff --git a/helm/ocaml/cic_proof_checking/cicElim.ml b/helm/ocaml/cic_proof_checking/cicElim.ml
index fb568613c943c8b3b7389d9d09d039d8e88b8046..60cf5af2e60031a37579b791985b287a63576a98 100644 (file)
--- a/helm/ocaml/cic_proof_checking/cicElim.ml
+++ b/helm/ocaml/cic_proof_checking/cicElim.ml
@@ -25,7 +25,7 @@
 
 open Printf
 
-exception Elim_failure of string
+exception Elim_failure of string Lazy.t
 exception Can_t_eliminate
 
 let debug_print = fun _ -> ()
@@ -382,9 +382,9 @@ debug_print (lazy (CicPp.ppterm eliminator_body));
         try
           CicTypeChecker.type_of_aux' [] [] eliminator_body CicUniv.empty_ugraph
         with CicTypeChecker.TypeCheckerFailure msg ->
-          raise (Elim_failure (sprintf 
+          raise (Elim_failure (lazy (sprintf 
             "type checker failure while type checking:\n%s\nerror:\n%s"
-            (CicPp.ppterm eliminator_body) msg))
+            (CicPp.ppterm eliminator_body) (Lazy.force msg))))
       in
       if not (fst (CicReduction.are_convertible []
         eliminator_type computed_type ugraph))