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.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/src/Util/ZUtil.v b/src/Util/ZUtil.v
index 319e018a9..d49c8eb8b 100644
--- a/src/Util/ZUtil.v
+++ b/src/Util/ZUtil.v
@@ -1249,7 +1249,7 @@ 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.
+ Existing Instance equiv_modulo_Reflexive | 10.
Existing Instance equiv_modulo_Symmetric.
Existing Instance equiv_modulo_Transitive.
Existing Instance mul_mod_Proper.