summaryrefslogtreecommitdiff
path: root/tactics/rewrite.ml4
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2012-03-27 07:43:43 +0200
committerGravatar Stephane Glondu <steph@glondu.net>2012-03-27 07:45:11 +0200
commit6e34b272d789455a9be589e27ad3a998cf25496b (patch)
tree57b74c7cbafd705a1ebce7d16cdaec02b704fb44 /tactics/rewrite.ml4
parent5fe4ac437bed43547b3695664974f492b55cb553 (diff)
parent2bdcd093b357adb2185518dabbafd1a0b9279044 (diff)
Remove non-DFSG contentsupstream/8.3.pl4+dfsg
Diffstat (limited to 'tactics/rewrite.ml4')
-rw-r--r--tactics/rewrite.ml42
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4
index fd3eeeb2..cf5fab0c 100644
--- a/tactics/rewrite.ml4
+++ b/tactics/rewrite.ml4
@@ -1057,7 +1057,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)))
+ | Compat.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."