diff options
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/refiner.ml | 6 | ||||
| -rw-r--r-- | proofs/refiner.mli | 3 |
2 files changed, 6 insertions, 3 deletions
diff --git a/proofs/refiner.ml b/proofs/refiner.ml index b0239eeb42..8b3789c3bb 100644 --- a/proofs/refiner.ml +++ b/proofs/refiner.ml @@ -335,10 +335,12 @@ let tclIDTAC_MESSAGE s gls = let tclFAIL_s s gls = errorlabstrm "Refiner.tclFAIL_s" (str s) (* A special exception for levels for the Fail tactic *) -exception FailError of int * std_ppcmds +exception FailError of int * std_ppcmds Lazy.t (* The Fail tactic *) -let tclFAIL lvl s g = raise (FailError (lvl,s)) +let tclFAIL lvl s g = raise (FailError (lvl,lazy s)) + +let tclFAIL_lazy lvl s g = raise (FailError (lvl,s)) let start_tac gls = let (sigr,g) = unpackage gls in diff --git a/proofs/refiner.mli b/proofs/refiner.mli index d6bd73ca48..9a587a9650 100644 --- a/proofs/refiner.mli +++ b/proofs/refiner.mli @@ -134,7 +134,7 @@ val tclTHENLASTn : tactic -> tactic array -> tactic val tclTHENFIRSTn : tactic -> tactic array -> tactic (* A special exception for levels for the Fail tactic *) -exception FailError of int * Pp.std_ppcmds +exception FailError of int * Pp.std_ppcmds Lazy.t (* Takes an exception and either raise it at the next level or do nothing. *) @@ -151,6 +151,7 @@ val tclTHENTRY : tactic -> tactic -> tactic val tclCOMPLETE : tactic -> tactic val tclAT_LEAST_ONCE : tactic -> tactic val tclFAIL : int -> Pp.std_ppcmds -> tactic +val tclFAIL_lazy : int -> Pp.std_ppcmds Lazy.t -> tactic val tclDO : int -> tactic -> tactic val tclPROGRESS : tactic -> tactic val tclWEAK_PROGRESS : tactic -> tactic |