From d28af587b9848c6155c7eae482591836f0fbc68f Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 26 Jun 2020 12:50:46 +0200
Subject: Move the FailError exception from Refiner to Tacticals.

---
 proofs/refiner.ml  | 11 -----------
 proofs/refiner.mli |  7 -------
 2 files changed, 18 deletions(-)

(limited to 'proofs')

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
-- 
cgit v1.2.3