From 568a48aa8c90b504029cc95480d81b5bd17b63ef Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Wed, 25 Mar 2020 11:51:27 -0400
Subject: Make the level of ≡ in Int63 consistent with =

Fixes #11905
---
 theories/Numbers/Cyclic/Int63/Int63.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'theories')

diff --git a/theories/Numbers/Cyclic/Int63/Int63.v b/theories/Numbers/Cyclic/Int63/Int63.v
index a8c645deb2..ca50470edc 100644
--- a/theories/Numbers/Cyclic/Int63/Int63.v
+++ b/theories/Numbers/Cyclic/Int63/Int63.v
@@ -690,7 +690,7 @@ Proof. now intros h; rewrite (to_Z_inj _ 0 h). Qed.
 Lemma tail00_spec x : φ  x = 0 -> φ (tail0 x) = φ digits.
 Proof. now intros h; rewrite (to_Z_inj _ 0 h). Qed.
 
-Infix "≡" := (eqm wB) (at level 80) : int63_scope.
+Infix "≡" := (eqm wB) (at level 70, no associativity) : int63_scope.
 
 Lemma eqm_mod x y : x mod wB ≡ y mod wB → x ≡ y.
 Proof.
-- 
cgit v1.2.3