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

[helm.git] / helm / ocaml / tactics / proofEngineReduction.ml

diff --git a/helm/ocaml/tactics/proofEngineReduction.ml b/helm/ocaml/tactics/proofEngineReduction.ml
index f8782b7aec13db70083d025a44258d1416d0cf21..fc3bfd3b8a66991101daa4dd029d07b039565171 100644 (file)
--- a/helm/ocaml/tactics/proofEngineReduction.ml
+++ b/helm/ocaml/tactics/proofEngineReduction.ml
@@ -909,14 +909,14 @@ let unfold ?what context where =
    | _,_ ->
      raise
       (ProofEngineTypes.Fail
-        "The term to unfold is not a constant, a variable or a bound variable ")
+        (lazy "The term to unfold is not a constant, a variable or a bound variable "))
  in
  let appl he tl =
   if tl = [] then he else Cic.Appl (he::tl) in
  let cannot_delta_expand t =
   raise
    (ProofEngineTypes.Fail
-     ("The term " ^ CicPp.ppterm t ^ " cannot be delta-expanded")) in
+     (lazy ("The term " ^ CicPp.ppterm t ^ " cannot be delta-expanded"))) in
  let rec hd_delta_beta context tl =
   function
     Cic.Rel n as t ->
@@ -967,7 +967,7 @@ let unfold ?what context where =
        if res = [] then
         raise
          (ProofEngineTypes.Fail
-           ("Term "^ CicPp.ppterm what ^ " not found in " ^ CicPp.ppterm where))
+           (lazy ("Term "^ CicPp.ppterm what ^ " not found in " ^ CicPp.ppterm where)))
        else
         res
  in