]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/tactics/fwdSimplTactic.ml
Every exception that used to have type string is now a string Lazy.t.
[helm.git] / helm / ocaml / tactics / fwdSimplTactic.ml
index bd2ac9fdeb7d85861cb6f130879ba61ced2d9bd5..16510a7cd9e456d5b25eaa9becf71e4d1f48613d 100644 (file)
@@ -38,7 +38,7 @@ module PESR = ProofEngineStructuralRules
 let fail_msg0 = "unexported clearbody: invalid argument"
 let fail_msg2 = "fwd: no applicable simplification"
 
-let error msg = raise (PET.Fail msg)
+let error msg = raise (PET.Fail (lazy msg))
 
 (* unexported tactics *******************************************************)