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.

---
 vernac/declare.ml | 2 +-
 vernac/himsg.ml   | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

(limited to 'vernac')

diff --git a/vernac/declare.ml b/vernac/declare.ml
index 6326a22e83..85359d5b62 100644
--- a/vernac/declare.ml
+++ b/vernac/declare.ml
@@ -2206,7 +2206,7 @@ let solve_by_tac ?loc name evi t ~poly ~uctx =
     Inductiveops.control_only_guard env (Evd.from_ctx uctx) (EConstr.of_constr body);
     Some (body, types, uctx)
   with
-  | Refiner.FailError (_, s) as exn ->
+  | Tacticals.FailError (_, s) as exn ->
     let _ = Exninfo.capture exn in
     CErrors.user_err ?loc ~hdr:"solve_obligation" (Lazy.force s)
   (* If the proof is open we absorb the error and leave the obligation open *)
diff --git a/vernac/himsg.ml b/vernac/himsg.ml
index 9d67ce3757..79f11fd6bc 100644
--- a/vernac/himsg.ml
+++ b/vernac/himsg.ml
@@ -1398,7 +1398,7 @@ let rec vernac_interp_error_handler = function
     str "The reference" ++ spc () ++ Libnames.pr_qualid q ++
     spc () ++ str "was not found" ++
     spc () ++ str "in the current" ++ spc () ++ str "environment."
-  | Refiner.FailError (i,s) ->
+  | Tacticals.FailError (i,s) ->
     let s = Lazy.force s in
     str "Tactic failure" ++
     (if Pp.ismt s then s else str ": " ++ s) ++
-- 
cgit v1.2.3