diff options
Diffstat (limited to 'proofs/refiner.mli')
| -rw-r--r-- | proofs/refiner.mli | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/proofs/refiner.mli b/proofs/refiner.mli index d6bd73ca4..9a587a965 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 |