Bring Int63 notations into line with stdlib

We also put them in a module, so users can `Require Int63. Import
Int63.Int63Notations` without needing to unqualify the primitives.

In particular, we change
- `a \% m` into `a mod m` to correspond with the notation in ZArith
- `m == n` into `m =? n` to correspond with the eqb notations elsewhere
- `m < n` into `m <? n` to correspond with the ltb notations elsewhere
- `m <= n` into `m <=? n` to correspond with the leb notations elsewhere
- `m ≤ n` into `m ≤? n` for consistency with the non-unicode notation

The old notations are still accessible as deprecated notations.

Fixes #12454

5 files changed, 44 insertions, 44 deletions

diff --git a/test-suite/primitive/uint63/eqb.v b/test-suite/primitive/uint63/eqb.v
index dcc0b71f6d..43c98e2b6f 100644
--- a/test-suite/primitive/uint63/eqb.v
+++ b/test-suite/primitive/uint63/eqb.v
@@ -4,14 +4,14 @@ Set Implicit Arguments.
 
 Open Scope int63_scope.
 
-Check (eq_refl : 1 == 1 = true).
-Check (eq_refl true <: 1 == 1 = true).
-Check (eq_refl true <<: 1 == 1 = true).
-Definition compute1 := Eval compute in 1 == 1.
+Check (eq_refl : 1 =? 1 = true).
+Check (eq_refl true <: 1 =? 1 = true).
+Check (eq_refl true <<: 1 =? 1 = true).
+Definition compute1 := Eval compute in 1 =? 1.
 Check (eq_refl compute1 : true = true).
 
-Check (eq_refl : 9223372036854775807 == 0 = false).
-Check (eq_refl false <: 9223372036854775807 == 0 = false).
-Check (eq_refl false <<: 9223372036854775807 == 0 = false).
-Definition compute2 := Eval compute in 9223372036854775807 == 0.
+Check (eq_refl : 9223372036854775807 =? 0 = false).
+Check (eq_refl false <: 9223372036854775807 =? 0 = false).
+Check (eq_refl false <<: 9223372036854775807 =? 0 = false).
+Definition compute2 := Eval compute in 9223372036854775807 =? 0.
 Check (eq_refl compute2 : false = false).
diff --git a/test-suite/primitive/uint63/leb.v b/test-suite/primitive/uint63/leb.v
index 5354919978..e5142282ae 100644
--- a/test-suite/primitive/uint63/leb.v
+++ b/test-suite/primitive/uint63/leb.v
@@ -4,20 +4,20 @@ Set Implicit Arguments.
 
 Open Scope int63_scope.
 
-Check (eq_refl : 1 <= 1 = true).
-Check (eq_refl true <: 1 <= 1 = true).
-Check (eq_refl true <<: 1 <= 1 = true).
-Definition compute1 := Eval compute in 1 <= 1.
+Check (eq_refl : 1 <=? 1 = true).
+Check (eq_refl true <: 1 <=? 1 = true).
+Check (eq_refl true <<: 1 <=? 1 = true).
+Definition compute1 := Eval compute in 1 <=? 1.
 Check (eq_refl compute1 : true = true).
 
-Check (eq_refl : 1 <= 2 = true).
-Check (eq_refl true <: 1 <= 2 = true).
-Check (eq_refl true <<: 1 <= 2 = true).
-Definition compute2 := Eval compute in 1 <= 2.
+Check (eq_refl : 1 <=? 2 = true).
+Check (eq_refl true <: 1 <=? 2 = true).
+Check (eq_refl true <<: 1 <=? 2 = true).
+Definition compute2 := Eval compute in 1 <=? 2.
 Check (eq_refl compute2 : true = true).
 
-Check (eq_refl : 9223372036854775807 <= 0 = false).
-Check (eq_refl false <: 9223372036854775807 <= 0 = false).
-Check (eq_refl false <<: 9223372036854775807 <= 0 = false).
-Definition compute3 := Eval compute in 9223372036854775807 <= 0.
+Check (eq_refl : 9223372036854775807 <=? 0 = false).
+Check (eq_refl false <: 9223372036854775807 <=? 0 = false).
+Check (eq_refl false <<: 9223372036854775807 <=? 0 = false).
+Definition compute3 := Eval compute in 9223372036854775807 <=? 0.
 Check (eq_refl compute3 : false = false).
diff --git a/test-suite/primitive/uint63/ltb.v b/test-suite/primitive/uint63/ltb.v
index 7ae5ac6493..50cef6be66 100644
--- a/test-suite/primitive/uint63/ltb.v
+++ b/test-suite/primitive/uint63/ltb.v
@@ -4,20 +4,20 @@ Set Implicit Arguments.
 
 Open Scope int63_scope.
 
-Check (eq_refl : 1 < 1 = false).
-Check (eq_refl false <: 1 < 1 = false).
-Check (eq_refl false <<: 1 < 1 = false).
-Definition compute1 := Eval compute in 1 < 1.
+Check (eq_refl : 1 <? 1 = false).
+Check (eq_refl false <: 1 <? 1 = false).
+Check (eq_refl false <<: 1 <? 1 = false).
+Definition compute1 := Eval compute in 1 <? 1.
 Check (eq_refl compute1 : false = false).
 
-Check (eq_refl : 1 < 2 = true).
-Check (eq_refl true <: 1 < 2 = true).
-Check (eq_refl true <<: 1 < 2 = true).
-Definition compute2 := Eval compute in 1 < 2.
+Check (eq_refl : 1 <? 2 = true).
+Check (eq_refl true <: 1 <? 2 = true).
+Check (eq_refl true <<: 1 <? 2 = true).
+Definition compute2 := Eval compute in 1 <? 2.
 Check (eq_refl compute2 : true = true).
 
-Check (eq_refl : 9223372036854775807 < 0 = false).
-Check (eq_refl false <: 9223372036854775807 < 0 = false).
-Check (eq_refl false <<: 9223372036854775807 < 0 = false).
-Definition compute3 := Eval compute in 9223372036854775807 < 0.
+Check (eq_refl : 9223372036854775807 <? 0 = false).
+Check (eq_refl false <: 9223372036854775807 <? 0 = false).
+Check (eq_refl false <<: 9223372036854775807 <? 0 = false).
+Definition compute3 := Eval compute in 9223372036854775807 <? 0.
 Check (eq_refl compute3 : false = false).
diff --git a/test-suite/primitive/uint63/mod.v b/test-suite/primitive/uint63/mod.v
index 5307eed493..3ad6312c2c 100644
--- a/test-suite/primitive/uint63/mod.v
+++ b/test-suite/primitive/uint63/mod.v
@@ -4,14 +4,14 @@ Set Implicit Arguments.
 
 Open Scope int63_scope.
 
-Check (eq_refl : 6 \% 3 = 0).
-Check (eq_refl 0 <: 6 \% 3 = 0).
-Check (eq_refl 0 <<: 6 \% 3 = 0).
-Definition compute1 := Eval compute in 6 \% 3.
+Check (eq_refl : 6 mod 3 = 0).
+Check (eq_refl 0 <: 6 mod 3 = 0).
+Check (eq_refl 0 <<: 6 mod 3 = 0).
+Definition compute1 := Eval compute in 6 mod 3.
 Check (eq_refl compute1 : 0 = 0).
 
-Check (eq_refl : 5 \% 3 = 2).
-Check (eq_refl 2 <: 5 \% 3 = 2).
-Check (eq_refl 2 <<: 5 \% 3 = 2).
-Definition compute2 := Eval compute in 5 \% 3.
+Check (eq_refl : 5 mod 3 = 2).
+Check (eq_refl 2 <: 5 mod 3 = 2).
+Check (eq_refl 2 <<: 5 mod 3 = 2).
+Definition compute2 := Eval compute in 5 mod 3.
 Check (eq_refl compute2 : 2 = 2).
diff --git a/test-suite/primitive/uint63/unsigned.v b/test-suite/primitive/uint63/unsigned.v
index 82920bd201..6224e9d15b 100644
--- a/test-suite/primitive/uint63/unsigned.v
+++ b/test-suite/primitive/uint63/unsigned.v
@@ -11,8 +11,8 @@ Check (eq_refl 0 <<: 1/(0-1) = 0).
 Definition compute1 := Eval compute in 1/(0-1).
 Check (eq_refl compute1 : 0 = 0).
 
-Check (eq_refl : 3 \% (0-1) = 3).
-Check (eq_refl 3 <: 3 \% (0-1) = 3).
-Check (eq_refl 3 <<: 3 \% (0-1) = 3).
-Definition compute2 := Eval compute in 3 \% (0-1).
+Check (eq_refl : 3 mod (0-1) = 3).
+Check (eq_refl 3 <: 3 mod (0-1) = 3).
+Check (eq_refl 3 <<: 3 mod (0-1) = 3).
+Definition compute2 := Eval compute in 3 mod (0-1).
 Check (eq_refl compute2 : 3 = 3).