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.

---
 plugins/ltac/rewrite.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'plugins/ltac/rewrite.ml')

diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index f16d0717df..40dea90c00 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -1567,7 +1567,7 @@ let assert_replacing id newt tac =
 
 let newfail n s =
   let info = Exninfo.reify () in
-  Proofview.tclZERO ~info (Refiner.FailError (n, lazy s))
+  Proofview.tclZERO ~info (Tacticals.FailError (n, lazy s))
 
 let cl_rewrite_clause_newtac ?abs ?origsigma ~progress strat clause =
   let open Proofview.Notations in
@@ -1656,7 +1656,7 @@ let cl_rewrite_clause_strat progress strat clause =
       (fun (e, info) -> match e with
        | RewriteFailure e ->
          tclZEROMSG ~info (str"setoid rewrite failed: " ++ e)
-       | Refiner.FailError (n, pp) ->
+       | Tacticals.FailError (n, pp) ->
          tclFAIL ~info n (str"setoid rewrite failed: " ++ Lazy.force pp)
        | e ->
          Proofview.tclZERO ~info e))
-- 
cgit v1.2.3