aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/rewrite.ml4
diff options
context:
space:
mode:
Diffstat (limited to 'tactics/rewrite.ml4')
-rw-r--r--tactics/rewrite.ml43
1 files changed, 2 insertions, 1 deletions
diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4
index d2381332e..4827c77b6 100644
--- a/tactics/rewrite.ml4
+++ b/tactics/rewrite.ml4
@@ -36,6 +36,7 @@ open Pfedit
open Command
open Libnames
open Evd
+open Compat
(** Typeclass-based generalized rewriting. *)
@@ -1052,7 +1053,7 @@ let cl_rewrite_clause_aux ?(abs=None) strat goal_meta clause gl =
else tclIDTAC
in tclTHENLIST [evartac; rewtac] gl
with
- | Stdpp.Exc_located (_, TypeClassError (env, (UnsatisfiableConstraints _ as e)))
+ | Loc.Exc_located (_, TypeClassError (env, (UnsatisfiableConstraints _ as e)))
| TypeClassError (env, (UnsatisfiableConstraints _ as e)) ->
Refiner.tclFAIL_lazy 0
(lazy (str"setoid rewrite failed: unable to satisfy the rewriting constraints."