X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Focaml%2Fcic_proof_checking%2FcicElim.ml;h=60cf5af2e60031a37579b791985b287a63576a98;hb=8b55faddb06e3c4b0a13839210bb49170939b33e;hp=fb568613c943c8b3b7389d9d09d039d8e88b8046;hpb=a93a94942ad58d8645af1fd94bef8fa31d9541a4;p=helm.git

diff --git a/helm/ocaml/cic_proof_checking/cicElim.ml b/helm/ocaml/cic_proof_checking/cicElim.ml
index fb568613c..60cf5af2e 100644
--- 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))