diff options
Diffstat (limited to 'proofs/refiner.mli')
| -rw-r--r-- | proofs/refiner.mli | 7 |
1 files changed, 0 insertions, 7 deletions
diff --git a/proofs/refiner.mli b/proofs/refiner.mli index e13e358d8f..c38cb23cb0 100644 --- a/proofs/refiner.mli +++ b/proofs/refiner.mli @@ -9,10 +9,3 @@ (************************************************************************) (** Legacy proof engine. Do not use in newly written code. *) - -(** A special exception for levels for the Fail tactic *) -exception FailError of int * Pp.t Lazy.t - -(** Takes an exception and either raise it at the next - level or do nothing. *) -val catch_failerror : Exninfo.iexn -> unit |