aboutsummaryrefslogtreecommitdiff
path: root/src/Util/ZUtil.v
diff options
context:
space:
mode:
Diffstat (limited to 'src/Util/ZUtil.v')
-rw-r--r--src/Util/ZUtil.v3
1 files changed, 2 insertions, 1 deletions
diff --git a/src/Util/ZUtil.v b/src/Util/ZUtil.v
index b448406fc..eeb99188b 100644
--- a/src/Util/ZUtil.v
+++ b/src/Util/ZUtil.v
@@ -1249,7 +1249,8 @@ Module Z.
End equiv_modulo.
Module EquivModuloInstances (dummy : Nop). (* work around https://coq.inria.fr/bugs/show_bug.cgi?id=4973 *)
- Existing Instance equiv_modulo_Reflexive | 10.
+ Existing Instance equiv_modulo_Reflexive.
+ Existing Instance eq_Reflexive. (* prioritize [Reflexive eq] *)
Existing Instance equiv_modulo_Symmetric.
Existing Instance equiv_modulo_Transitive.
Existing Instance mul_mod_Proper.