diff options
| author | Pierre-Marie Pédrot | 2020-06-26 12:50:46 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-06-29 15:20:35 +0200 |
| commit | d28af587b9848c6155c7eae482591836f0fbc68f (patch) | |
| tree | f485f9cd2c05bd05d2b02c832fe732f1419004e0 /proofs | |
| parent | f34dcb97406611704c93970ea623d6a8587e5ba8 (diff) | |
Move the FailError exception from Refiner to Tacticals.
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/refiner.ml | 11 | ||||
| -rw-r--r-- | proofs/refiner.mli | 7 |
2 files changed, 0 insertions, 18 deletions
diff --git a/proofs/refiner.ml b/proofs/refiner.ml index cd44b2ae71..b72d544151 100644 --- a/proofs/refiner.ml +++ b/proofs/refiner.ml @@ -7,14 +7,3 @@ (* * GNU Lesser General Public License Version 2.1 *) (* * (see LICENSE file for the text of the license) *) (************************************************************************) - -open Util - -(* A special exception for levels for the Fail tactic *) -exception FailError of int * Pp.t Lazy.t - -let catch_failerror (e, info) = - match e with - | FailError (lvl,s) when lvl > 0 -> - Exninfo.iraise (FailError (lvl - 1, s), info) - | e -> Control.check_for_interrupt () 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 |