diff options
Diffstat (limited to 'proofs/refiner.ml')
| -rw-r--r-- | proofs/refiner.ml | 11 |
1 files changed, 0 insertions, 11 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 () |