Merge PR #13559: Signed primitive integers

Reviewed-by: SkySkimmer
Reviewed-by: silene
Reviewed-by: jfehrle
Ack-by: gares
Ack-by: Zimmi48
Ack-by: proux01

13 files changed, 462 insertions, 0 deletions

diff --git a/test-suite/primitive/sint63/add.v b/test-suite/primitive/sint63/add.v
new file mode 100644
index 0000000000..dcafd64181
--- /dev/null
+++ b/test-suite/primitive/sint63/add.v
@@ -0,0 +1,25 @@
+Require Import Sint63.
+
+Set Implicit Arguments.
+
+Open Scope sint63_scope.
+
+Check (eq_refl : 2 + 3 = 5).
+Check (eq_refl 5 <: 2 + 3 = 5).
+Check (eq_refl 5 <<: 2 + 3 = 5).
+Definition compute1 := Eval compute in 2 + 3.
+Check (eq_refl compute1 : 5 = 5).
+
+Check (eq_refl : 4611686018427387903 + 1 = -4611686018427387904).
+Check (eq_refl (-4611686018427387904) <:
+  4611686018427387903 + 1 = -4611686018427387904).
+Check (eq_refl (-4611686018427387904) <<:
+  4611686018427387903 + 1 = -4611686018427387904).
+Definition compute2 := Eval compute in 4611686018427387903 + 1.
+Check (eq_refl compute2 : -4611686018427387904 = -4611686018427387904).
+
+Check (eq_refl : 2 - 3 = -1).
+Check (eq_refl (-1) <: 2 - 3 = -1).
+Check (eq_refl (-1) <<: 2 - 3 = -1).
+Definition compute3 := Eval compute in 2 - 3.
+Check (eq_refl compute3 : -1 = -1).
diff --git a/test-suite/primitive/sint63/asr.v b/test-suite/primitive/sint63/asr.v
new file mode 100644
index 0000000000..4524ae4e6f
--- /dev/null
+++ b/test-suite/primitive/sint63/asr.v
@@ -0,0 +1,41 @@
+Require Import Sint63.
+
+Set Implicit Arguments.
+
+Open Scope sint63_scope.
+
+Check (eq_refl : (-2305843009213693952) >> 61 = -1).
+Check (eq_refl (-1) <: (-2305843009213693952) >> 61 = -1).
+Check (eq_refl (-1) <<: (-2305843009213693952) >> 61 = -1).
+Definition compute1 := Eval compute in (-2305843009213693952) >> 61.
+Check (eq_refl compute1 : -1 = -1).
+
+Check (eq_refl : 2305843009213693952 >> 62 = 0).
+Check (eq_refl 0 <: 2305843009213693952 >> 62 = 0).
+Check (eq_refl 0 <<: 2305843009213693952 >> 62 = 0).
+Definition compute2 := Eval compute in 2305843009213693952 >> 62.
+Check (eq_refl compute2 : 0 = 0).
+
+Check (eq_refl : 4611686018427387903 >> 63 = 0).
+Check (eq_refl 0 <: 4611686018427387903 >> 63 = 0).
+Check (eq_refl 0 <<: 4611686018427387903 >> 63 = 0).
+Definition compute3 := Eval compute in 4611686018427387903 >> 63.
+Check (eq_refl compute3 : 0 = 0).
+
+Check (eq_refl : (-1) >> 1 = -1).
+Check (eq_refl (-1) <: (-1) >> 1 = -1).
+Check (eq_refl (-1) <<: (-1) >> 1 = -1).
+Definition compute4 := Eval compute in (-1) >> 1.
+Check (eq_refl compute4 : -1 = -1).
+
+Check (eq_refl : (-1) >> (-1) = 0).
+Check (eq_refl 0 <: (-1) >> (-1) = 0).
+Check (eq_refl 0 <<: (-1) >> (-1) = 0).
+Definition compute5 := Eval compute in (-1) >> (-1).
+Check (eq_refl compute5 : 0 = 0).
+
+Check (eq_refl : 73 >> (-2) = 0).
+Check (eq_refl 0 <: 73 >> (-2) = 0).
+Check (eq_refl 0 <<: 73 >> (-2) = 0).
+Definition compute6 := Eval compute in 73 >> (-2).
+Check (eq_refl compute6 : 0 = 0).
diff --git a/test-suite/primitive/sint63/compare.v b/test-suite/primitive/sint63/compare.v
new file mode 100644
index 0000000000..7a9882f1c8
--- /dev/null
+++ b/test-suite/primitive/sint63/compare.v
@@ -0,0 +1,36 @@
+Require Import Sint63.
+
+Set Implicit Arguments.
+
+Open Scope sint63_scope.
+
+Check (eq_refl : 1 ?= 1 = Eq).
+Check (eq_refl Eq <: 1 ?= 1 = Eq).
+Check (eq_refl Eq <<: 1 ?= 1 = Eq).
+Definition compute1 := Eval compute in 1 ?= 1.
+Check (eq_refl compute1 : Eq = Eq).
+
+Check (eq_refl : 1 ?= 2 = Lt).
+Check (eq_refl Lt <: 1 ?= 2 = Lt).
+Check (eq_refl Lt <<: 1 ?= 2 = Lt).
+Definition compute2 := Eval compute in 1 ?= 2.
+Check (eq_refl compute2 : Lt = Lt).
+
+Check (eq_refl : 4611686018427387903 ?= 0 = Gt).
+Check (eq_refl Gt <: 4611686018427387903 ?= 0 = Gt).
+Check (eq_refl Gt <<: 4611686018427387903 ?= 0 = Gt).
+Definition compute3 := Eval compute in 4611686018427387903 ?= 0.
+Check (eq_refl compute3 : Gt = Gt).
+
+Check (eq_refl : -1 ?= 1 = Lt).
+Check (eq_refl Lt <: -1 ?= 1 = Lt).
+Check (eq_refl Lt <<: -1 ?= 1 = Lt).
+Definition compute4 := Eval compute in -1 ?= 1.
+Check (eq_refl compute4 : Lt = Lt).
+
+Check (eq_refl : 4611686018427387903 ?= -4611686018427387904 = Gt).
+Check (eq_refl Gt <: 4611686018427387903 ?= -4611686018427387904 = Gt).
+Check (eq_refl Gt <<: 4611686018427387903 ?= -4611686018427387904 = Gt).
+Definition compute5 :=
+  Eval compute in 4611686018427387903 ?= -4611686018427387904.
+Check (eq_refl compute5 : Gt = Gt).
diff --git a/test-suite/primitive/sint63/div.v b/test-suite/primitive/sint63/div.v
new file mode 100644
index 0000000000..9da628ce1e
--- /dev/null
+++ b/test-suite/primitive/sint63/div.v
@@ -0,0 +1,61 @@
+Require Import Sint63.
+
+Set Implicit Arguments.
+
+Open Scope sint63_scope.
+
+Check (eq_refl : 6 / 3 = 2).
+Check (eq_refl 2 <: 6 / 3 = 2).
+Check (eq_refl 2 <<: 6 / 3 = 2).
+Definition compute1 := Eval compute in 6 / 3.
+Check (eq_refl compute1 : 2 = 2).
+
+Check (eq_refl : -6 / 3 = -2).
+Check (eq_refl (-2) <: -6 / 3 = -2).
+Check (eq_refl (-2) <<: -6 / 3 = -2).
+Definition compute2 := Eval compute in -6 / 3.
+Check (eq_refl compute2 : -2 = -2).
+
+Check (eq_refl : 6 / -3 = -2).
+Check (eq_refl (-2) <: 6 / -3 = -2).
+Check (eq_refl (-2) <<: 6 / -3 = -2).
+Definition compute3 := Eval compute in 6 / -3.
+Check (eq_refl compute3 : -2 = -2).
+
+Check (eq_refl : -6 / -3 = 2).
+Check (eq_refl 2 <: -6 / -3 = 2).
+Check (eq_refl 2 <<: -6 / -3 = 2).
+Definition compute4 := Eval compute in -6 / -3.
+Check (eq_refl compute4 : 2 = 2).
+
+Check (eq_refl : 3 / 2 = 1).
+Check (eq_refl 1 <: 3 / 2 = 1).
+Check (eq_refl 1 <<: 3 / 2 = 1).
+Definition compute5 := Eval compute in 3 / 2.
+Check (eq_refl compute5 : 1 = 1).
+
+Check (eq_refl : -3 / 2 = -1).
+Check (eq_refl (-1) <: -3 / 2 = -1).
+Check (eq_refl (-1) <<: -3 / 2 = -1).
+Definition compute6 := Eval compute in -3 / 2.
+Check (eq_refl compute6 : -1 = -1).
+
+Check (eq_refl : 3 / -2 = -1).
+Check (eq_refl (-1) <: 3 / -2 = -1).
+Check (eq_refl (-1) <<: 3 / -2 = -1).
+Definition compute7 := Eval compute in 3 / -2.
+Check (eq_refl compute7 : -1 = -1).
+
+Check (eq_refl : -3 / -2 = 1).
+Check (eq_refl 1 <: -3 / -2 = 1).
+Check (eq_refl 1 <<: -3 / -2 = 1).
+Definition compute8 := Eval compute in -3 / -2.
+Check (eq_refl compute8 : 1 = 1).
+
+Check (eq_refl : -4611686018427387904 / -1 = -4611686018427387904).
+Check (eq_refl (-4611686018427387904) <:
+  -4611686018427387904 / -1 = -4611686018427387904).
+Check (eq_refl (-4611686018427387904) <<:
+  -4611686018427387904 / -1 = -4611686018427387904).
+Definition compute9 := Eval compute in -4611686018427387904 / -1.
+Check (eq_refl compute9 : -4611686018427387904 = -4611686018427387904).
diff --git a/test-suite/primitive/sint63/eqb.v b/test-suite/primitive/sint63/eqb.v
new file mode 100644
index 0000000000..4d365acf54
--- /dev/null
+++ b/test-suite/primitive/sint63/eqb.v
@@ -0,0 +1,17 @@
+Require Import Sint63.
+
+Set Implicit Arguments.
+
+Open Scope sint63_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 compute1 : true = true).
+
+Check (eq_refl : 4611686018427387903 =? 0 = false).
+Check (eq_refl false <: 4611686018427387903 =? 0 = false).
+Check (eq_refl false <<: 4611686018427387903 =? 0 = false).
+Definition compute2 := Eval compute in 4611686018427387903 =? 0.
+Check (eq_refl compute2 : false = false).
diff --git a/test-suite/primitive/sint63/isint.v b/test-suite/primitive/sint63/isint.v
new file mode 100644
index 0000000000..f1c9c2cfd1
--- /dev/null
+++ b/test-suite/primitive/sint63/isint.v
@@ -0,0 +1,50 @@
+(* This file tests the check that arithmetic operations use to know if their
+arguments are ground. The various test cases correspond to possible
+optimizations of these tests made by the compiler. *)
+Require Import Sint63.
+
+Set Implicit Arguments.
+
+Open Scope sint63_scope.
+
+Section test.
+
+Variable m n : int.
+
+Check (eq_refl : (fun x => x + 3) m = m + 3).
+Check (eq_refl (m + 3) <: (fun x => x + 3) m = m + 3).
+Check (eq_refl (m + 3) <<: (fun x => x + 3) m = m + 3).
+Definition compute1 := Eval compute in (fun x => x + 3) m.
+Check (eq_refl compute1 : m + 3 = m + 3).
+
+Check (eq_refl : (fun x => 3 + x) m = 3 + m).
+Check (eq_refl (3 + m) <: (fun x => 3 + x) m = 3 + m).
+Check (eq_refl (3 + m) <<: (fun x => 3 + x) m = 3 + m).
+Definition compute2 := Eval compute in (fun x => 3 + x) m.
+Check (eq_refl compute2 : 3 + m = 3 + m).
+
+Check (eq_refl : (fun x y => x + y) m n = m + n).
+Check (eq_refl (m + n) <: (fun x y => x + y) m n = m + n).
+Check (eq_refl (m + n) <<: (fun x y => x + y) m n = m + n).
+Definition compute3 := Eval compute in (fun x y => x + y) m n.
+Check (eq_refl compute3 : m + n = m + n).
+
+Check (eq_refl : (fun x y => x + y) 2 3 = 5).
+Check (eq_refl 5 <: (fun x y => x + y) 2 3 = 5).
+Check (eq_refl 5 <<: (fun x y => x + y) 2 3 = 5).
+Definition compute4 := Eval compute in (fun x y => x + y) 2 3.
+Check (eq_refl compute4 : 5 = 5).
+
+Check (eq_refl : (fun x => x + x) m = m + m).
+Check (eq_refl (m + m) <: (fun x => x + x) m = m + m).
+Check (eq_refl (m + m) <<: (fun x => x + x) m = m + m).
+Definition compute5 := Eval compute in (fun x => x + x) m.
+Check (eq_refl compute5 : m + m = m + m).
+
+Check (eq_refl : (fun x => x + x) 2 = 4).
+Check (eq_refl 4 <: (fun x => x + x) 2 = 4).
+Check (eq_refl 4 <<: (fun x => x + x) 2 = 4).
+Definition compute6 := Eval compute in (fun x => x + x) 2.
+Check (eq_refl compute6 : 4 = 4).
+
+End test.
diff --git a/test-suite/primitive/sint63/leb.v b/test-suite/primitive/sint63/leb.v
new file mode 100644
index 0000000000..dbe958e41d
--- /dev/null
+++ b/test-suite/primitive/sint63/leb.v
@@ -0,0 +1,29 @@
+Require Import Sint63.
+
+Set Implicit Arguments.
+
+Open Scope sint63_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 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 compute2 : true = true).
+
+Check (eq_refl : 4611686018427387903 <=? 0 = false).
+Check (eq_refl false <: 4611686018427387903 <=? 0 = false).
+Check (eq_refl false <<: 4611686018427387903 <=? 0 = false).
+Definition compute3 := Eval compute in 4611686018427387903 <=? 0.
+Check (eq_refl compute3 : false = false).
+
+Check (eq_refl : 1 <=? -1 = false).
+Check (eq_refl false <: 1 <=? -1 = false).
+Check (eq_refl false <<: 1 <=? -1 = false).
+Definition compute4 := Eval compute in 1 <=? -1.
+Check (eq_refl compute4 : false = false).
diff --git a/test-suite/primitive/sint63/lsl.v b/test-suite/primitive/sint63/lsl.v
new file mode 100644
index 0000000000..082c42979a
--- /dev/null
+++ b/test-suite/primitive/sint63/lsl.v
@@ -0,0 +1,43 @@
+Require Import Sint63.
+
+Set Implicit Arguments.
+
+Open Scope sint63_scope.
+
+Check (eq_refl : 3 << 61 = -2305843009213693952).
+Check (eq_refl (-2305843009213693952) <: 3 << 61 = -2305843009213693952).
+Check (eq_refl (-2305843009213693952) <<: 3 << 61 = -2305843009213693952).
+Definition compute1 := Eval compute in 3 << 61.
+Check (eq_refl compute1 : -2305843009213693952 = -2305843009213693952).
+
+Check (eq_refl : 2 << 62 = 0).
+Check (eq_refl 0 <: 2 << 62 = 0).
+Check (eq_refl 0 <<: 2 << 62 = 0).
+Definition compute2 := Eval compute in 2 << 62.
+Check (eq_refl compute2 : 0 = 0).
+
+Check (eq_refl : 4611686018427387903 << 63 = 0).
+Check (eq_refl 0 <: 4611686018427387903 << 63 = 0).
+Check (eq_refl 0 <<: 4611686018427387903 << 63 = 0).
+Definition compute3 := Eval compute in 4611686018427387903 << 63.
+Check (eq_refl compute3 : 0 = 0).
+
+Check (eq_refl : 4611686018427387903 << 62 = -4611686018427387904).
+Check (eq_refl (-4611686018427387904) <:
+  4611686018427387903 << 62 = -4611686018427387904).
+Check (eq_refl (-4611686018427387904) <<:
+  4611686018427387903 << 62 = -4611686018427387904).
+Definition compute4 := Eval compute in 4611686018427387903 << 62.
+Check (eq_refl compute4 : -4611686018427387904 = -4611686018427387904).
+
+Check (eq_refl : 1 << 62 = -4611686018427387904).
+Check (eq_refl (-4611686018427387904) <: 1 << 62 = -4611686018427387904).
+Check (eq_refl (-4611686018427387904) <<: 1 << 62 = -4611686018427387904).
+Definition compute5 := Eval compute in 1 << 62.
+Check (eq_refl compute5 : -4611686018427387904 = -4611686018427387904).
+
+Check (eq_refl : -1 << 1 = -2).
+Check (eq_refl (-2) <: -1 << 1 = -2).
+Check (eq_refl (-2) <<: -1 << 1 = -2).
+Definition compute6 := Eval compute in -1 << 1.
+Check (eq_refl compute6 : -2 = -2).
diff --git a/test-suite/primitive/sint63/ltb.v b/test-suite/primitive/sint63/ltb.v
new file mode 100644
index 0000000000..aa72e1d377
--- /dev/null
+++ b/test-suite/primitive/sint63/ltb.v
@@ -0,0 +1,29 @@
+Require Import Sint63.
+
+Set Implicit Arguments.
+
+Open Scope sint63_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 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 compute2 : true = true).
+
+Check (eq_refl : 4611686018427387903 <? 0 = false).
+Check (eq_refl false <: 4611686018427387903 <? 0 = false).
+Check (eq_refl false <<: 4611686018427387903 <? 0 = false).
+Definition compute3 := Eval compute in 4611686018427387903 <? 0.
+Check (eq_refl compute3 : false = false).
+
+Check (eq_refl : 1 <? -1 = false).
+Check (eq_refl false <: 1 <? -1 = false).
+Check (eq_refl false <<: 1 <? -1 = false).
+Definition compute4 := Eval compute in 1 <? -1.
+Check (eq_refl compute4 : false = false).
diff --git a/test-suite/primitive/sint63/mod.v b/test-suite/primitive/sint63/mod.v
new file mode 100644
index 0000000000..a4872b45f3
--- /dev/null
+++ b/test-suite/primitive/sint63/mod.v
@@ -0,0 +1,53 @@
+Require Import Sint63.
+
+Set Implicit Arguments.
+
+Open Scope sint63_scope.
+
+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 : -6 mod 3 = 0).
+Check (eq_refl 0 <: -6 mod 3 = 0).
+Check (eq_refl 0 <<: -6 mod 3 = 0).
+Definition compute2 := Eval compute in -6 mod 3.
+Check (eq_refl compute2 : 0 = 0).
+
+Check (eq_refl : 6 mod -3 = 0).
+Check (eq_refl 0 <: 6 mod -3 = 0).
+Check (eq_refl 0 <<: 6 mod -3 = 0).
+Definition compute3 := Eval compute in 6 mod -3.
+Check (eq_refl compute3 : 0 = 0).
+
+Check (eq_refl : -6 mod -3 = 0).
+Check (eq_refl 0 <: -6 mod -3 = 0).
+Check (eq_refl 0 <<: -6 mod -3 = 0).
+Definition compute4 := Eval compute in -6 mod -3.
+Check (eq_refl compute4 : 0 = 0).
+
+Check (eq_refl : 5 mod 3 = 2).
+Check (eq_refl 2 <: 5 mod 3 = 2).
+Check (eq_refl 2 <<: 5 mod 3 = 2).
+Definition compute5 := Eval compute in 5 mod 3.
+Check (eq_refl compute5 : 2 = 2).
+
+Check (eq_refl : -5 mod 3 = -2).
+Check (eq_refl (-2) <: -5 mod 3 = -2).
+Check (eq_refl (-2) <<: -5 mod 3 = -2).
+Definition compute6 := Eval compute in -5 mod 3.
+Check (eq_refl compute6 : -2 = -2).
+
+Check (eq_refl : 5 mod -3 = 2).
+Check (eq_refl 2 <: 5 mod -3 = 2).
+Check (eq_refl 2 <<: 5 mod -3 = 2).
+Definition compute7 := Eval compute in 5 mod -3.
+Check (eq_refl compute7 : 2 = 2).
+
+Check (eq_refl : -5 mod -3 = -2).
+Check (eq_refl (-2) <: -5 mod -3 = -2).
+Check (eq_refl (-2) <<: -5 mod -3 = -2).
+Definition compute8 := Eval compute in -5 mod -3.
+Check (eq_refl compute8 : -2 = -2).
diff --git a/test-suite/primitive/sint63/mul.v b/test-suite/primitive/sint63/mul.v
new file mode 100644
index 0000000000..f72f643083
--- /dev/null
+++ b/test-suite/primitive/sint63/mul.v
@@ -0,0 +1,35 @@
+Require Import Sint63.
+
+Set Implicit Arguments.
+
+Open Scope sint63_scope.
+
+Check (eq_refl : 2 * 3 = 6).
+Check (eq_refl 6 <: 2 * 3 = 6).
+Check (eq_refl 6 <<: 2 * 3 = 6).
+Definition compute1 := Eval compute in 2 * 3.
+Check (eq_refl compute1 : 6 = 6).
+
+Check (eq_refl : -2 * 3 = -6).
+Check (eq_refl (-6) <: -2 * 3 = -6).
+Check (eq_refl (-6) <<: -2 * 3 = -6).
+Definition compute2 := Eval compute in -2 * 3.
+Check (eq_refl compute2 : -6 = -6).
+
+Check (eq_refl : 2 * -3 = -6).
+Check (eq_refl (-6) <: 2 * -3 = -6).
+Check (eq_refl (-6) <<: 2 * -3 = -6).
+Definition compute3 := Eval compute in 2 * -3.
+Check (eq_refl compute3 : -6 = -6).
+
+Check (eq_refl : -2 * -3 = 6).
+Check (eq_refl 6 <: -2 * -3 = 6).
+Check (eq_refl 6 <<: -2 * -3 = 6).
+Definition compute4 := Eval compute in -2 * -3.
+Check (eq_refl compute4 : 6 = 6).
+
+Check (eq_refl : 4611686018427387903 * 2 = -2).
+Check (eq_refl (-2) <: 4611686018427387903 * 2 = -2).
+Check (eq_refl (-2) <<: 4611686018427387903 * 2 = -2).
+Definition compute5 := Eval compute in 4611686018427387903 * 2.
+Check (eq_refl compute5 : -2 = -2).
diff --git a/test-suite/primitive/sint63/signed.v b/test-suite/primitive/sint63/signed.v
new file mode 100644
index 0000000000..d8333a8efb
--- /dev/null
+++ b/test-suite/primitive/sint63/signed.v
@@ -0,0 +1,18 @@
+(* This file checks that operations over sint63 are signed. *)
+Require Import Sint63.
+
+Open Scope sint63_scope.
+
+(* (0-1) must be negative 1 and not the maximum integer value *)
+
+Check (eq_refl : 1/(0-1) = -1).
+Check (eq_refl (-1) <: 1/(0-1) = -1).
+Check (eq_refl (-1) <<: 1/(0-1) = -1).
+Definition compute1 := Eval compute in 1/(0-1).
+Check (eq_refl compute1 : -1 = -1).
+
+Check (eq_refl : 3 mod (0-1) = 0).
+Check (eq_refl 0 <: 3 mod (0-1) = 0).
+Check (eq_refl 0 <<: 3 mod (0-1) = 0).
+Definition compute2 := Eval compute in 3 mod (0-1).
+Check (eq_refl compute2 : 0 = 0).
diff --git a/test-suite/primitive/sint63/sub.v b/test-suite/primitive/sint63/sub.v
new file mode 100644
index 0000000000..8504177286
--- /dev/null
+++ b/test-suite/primitive/sint63/sub.v
@@ -0,0 +1,25 @@
+Require Import Sint63.
+
+Set Implicit Arguments.
+
+Open Scope sint63_scope.
+
+Check (eq_refl : 3 - 2 = 1).
+Check (eq_refl 1 <: 3 - 2 = 1).
+Check (eq_refl 1 <<: 3 - 2 = 1).
+Definition compute1 := Eval compute in 3 - 2.
+Check (eq_refl compute1 : 1 = 1).
+
+Check (eq_refl : 0 - 1 = -1).
+Check (eq_refl (-1) <: 0 - 1 = -1).
+Check (eq_refl (-1) <<: 0 - 1 = -1).
+Definition compute2 := Eval compute in 0 - 1.
+Check (eq_refl compute2 : -1 = -1).
+
+Check (eq_refl : -4611686018427387904 - 1 = 4611686018427387903).
+Check (eq_refl 4611686018427387903 <:
+  -4611686018427387904 - 1 = 4611686018427387903).
+Check (eq_refl 4611686018427387903 <<:
+  -4611686018427387904 - 1 = 4611686018427387903).
+Definition compute3 := Eval compute in -4611686018427387904 - 1.
+Check (eq_refl compute3 : 4611686018427387903 = 4611686018427387903).