Merge PR #13559: Signed primitive integers

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

21 files changed, 607 insertions, 17 deletions

diff --git a/test-suite/output/Int63Syntax.out b/test-suite/output/Int63Syntax.out
index 7ca4de1e46..96af456891 100644
--- a/test-suite/output/Int63Syntax.out
+++ b/test-suite/output/Int63Syntax.out
@@ -15,9 +15,9 @@
 427
      : int
 The command has indeed failed with message:
-Cannot interpret this number as a value of type Coq.Numbers.Cyclic.Int63.PrimInt63.int
+Cannot interpret this number as a value of type int
 The command has indeed failed with message:
-Cannot interpret this number as a value of type Coq.Numbers.Cyclic.Int63.PrimInt63.int
+Cannot interpret this number as a value of type int
 0
      : int
 0
@@ -33,9 +33,11 @@ The reference x was not found in the current environment.
 add 2 2
      : int
 The command has indeed failed with message:
-int63 are only non-negative numbers.
+Cannot interpret this number as a value of type int
 The command has indeed failed with message:
 overflow in int63 literal: 9223372036854775808
+0x1
+     : int
 2
      : nat
 2%int63
diff --git a/test-suite/output/Int63Syntax.v b/test-suite/output/Int63Syntax.v
index 50910264f2..be0ee701af 100644
--- a/test-suite/output/Int63Syntax.v
+++ b/test-suite/output/Int63Syntax.v
@@ -20,6 +20,11 @@ Fail Check 0x.
 Check (PrimInt63.add 2 2).
 Fail Check -1.
 Fail Check 9223372036854775808.
+
+Set Printing All.
+Check 1%int63.
+Unset Printing All.
+
 Open Scope nat_scope.
 Check 2. (* : nat *)
 Check 2%int63.
diff --git a/test-suite/output/Notations4.out b/test-suite/output/Notations4.out
index 3477a293e3..0b18981f4e 100644
--- a/test-suite/output/Notations4.out
+++ b/test-suite/output/Notations4.out
@@ -77,18 +77,18 @@ fun x : nat => [x]
      : nat -> nat
 ∀ x : nat, x = x
      : Prop
-File "stdin", line 184, characters 0-160:
+File "stdin", line 187, characters 0-160:
 Warning: Notation "∀ _ .. _ , _" was already defined with a different format
 in scope type_scope. [notation-incompatible-format,parsing]
 ∀x : nat,x = x
      : Prop
-File "stdin", line 197, characters 0-60:
+File "stdin", line 200, characters 0-60:
 Warning: Notation "_ %%% _" was already defined with a different format.
 [notation-incompatible-format,parsing]
-File "stdin", line 201, characters 0-64:
+File "stdin", line 204, characters 0-64:
 Warning: Notation "_ %%% _" was already defined with a different format.
 [notation-incompatible-format,parsing]
-File "stdin", line 206, characters 0-62:
+File "stdin", line 209, characters 0-62:
 Warning: Lonely notation "_ %%%% _" was already defined with a different
 format. [notation-incompatible-format,parsing]
 3  %%  4
@@ -97,10 +97,10 @@ format. [notation-incompatible-format,parsing]
      : nat
 3   %%   4
      : nat
-File "stdin", line 234, characters 0-61:
+File "stdin", line 237, characters 0-61:
 Warning: The format modifier is irrelevant for only parsing rules.
 [irrelevant-format-only-parsing,parsing]
-File "stdin", line 238, characters 0-63:
+File "stdin", line 241, characters 0-63:
 Warning: The only parsing modifier has no effect in Reserved Notation.
 [irrelevant-reserved-notation-only-parsing,parsing]
 fun x : nat => U (S x)
@@ -111,7 +111,7 @@ fun x : nat => V x
      : forall x : nat, nat * (?T -> ?T)
 where
 ?T : [x : nat  x0 : ?T |- Type] (x0 cannot be used)
-File "stdin", line 255, characters 0-30:
+File "stdin", line 258, characters 0-30:
 Warning: Notation "_ :=: _" was already used. [notation-overridden,parsing]
 0 :=: 0
      : Prop
diff --git a/test-suite/output/Notations4.v b/test-suite/output/Notations4.v
index ebad12af88..a5ec92fe3c 100644
--- a/test-suite/output/Notations4.v
+++ b/test-suite/output/Notations4.v
@@ -103,7 +103,10 @@ Module NumberNotations.
     Delimit Scope test17_scope with test17.
     Local Set Primitive Projections.
     Record myint63 := of_int { to_int : int }.
-    Number Notation myint63 of_int to_int : test17_scope.
+    Definition parse x :=
+      match x with Pos x => Some (of_int x) | Neg _ => None end.
+    Definition print x := Pos (to_int x).
+    Number Notation myint63 parse print : test17_scope.
     Check let v := 0%test17 in v : myint63.
   End Test17.
 End NumberNotations.
diff --git a/test-suite/output/NumberNotations.out b/test-suite/output/NumberNotations.out
index 60682edec8..df9b39389c 100644
--- a/test-suite/output/NumberNotations.out
+++ b/test-suite/output/NumberNotations.out
@@ -260,28 +260,28 @@ The command has indeed failed with message:
 add is not a constructor of an inductive type.
 The command has indeed failed with message:
 Missing mapping for constructor Iempty.
-File "stdin", line 574, characters 56-61:
+File "stdin", line 577, characters 56-61:
 Warning: Type of I'sum seems incompatible with the type of sum.
 Expected type is: (I' -> I' -> I') instead of (I -> I' -> I').
 This might yield ill typed terms when using the notation.
 [via-type-mismatch,numbers]
-File "stdin", line 579, characters 32-33:
+File "stdin", line 582, characters 32-33:
 Warning: I was already mapped to Set, mapping it also to
 nat might yield ill typed terms when using the notation.
 [via-type-remapping,numbers]
-File "stdin", line 579, characters 37-42:
+File "stdin", line 582, characters 37-42:
 Warning: Type of Iunit seems incompatible with the type of O.
 Expected type is: I instead of I.
 This might yield ill typed terms when using the notation.
 [via-type-mismatch,numbers]
 The command has indeed failed with message:
 'via' and 'abstract' cannot be used together.
-File "stdin", line 659, characters 21-23:
+File "stdin", line 662, characters 21-23:
 Warning: Type of I1 seems incompatible with the type of Fin.F1.
 Expected type is: (nat -> I) instead of I.
 This might yield ill typed terms when using the notation.
 [via-type-mismatch,numbers]
-File "stdin", line 659, characters 35-37:
+File "stdin", line 662, characters 35-37:
 Warning: Type of IS seems incompatible with the type of Fin.FS.
 Expected type is: (nat -> I -> I) instead of (I -> I).
 This might yield ill typed terms when using the notation.
diff --git a/test-suite/output/NumberNotations.v b/test-suite/output/NumberNotations.v
index 718da13500..85400c2fd4 100644
--- a/test-suite/output/NumberNotations.v
+++ b/test-suite/output/NumberNotations.v
@@ -328,7 +328,10 @@ Module Test17.
   Delimit Scope test17_scope with test17.
   Local Set Primitive Projections.
   Record myint63 := of_int { to_int : int }.
-  Number Notation myint63 of_int to_int : test17_scope.
+  Definition parse x :=
+    match x with Pos x => Some (of_int x) | Neg _ => None end.
+  Definition print x := Pos (to_int x).
+  Number Notation myint63 parse print : test17_scope.
   Check let v := 0%test17 in v : myint63.
 End Test17.
 
diff --git a/test-suite/output/Sint63Syntax.out b/test-suite/output/Sint63Syntax.out
new file mode 100644
index 0000000000..db14658307
--- /dev/null
+++ b/test-suite/output/Sint63Syntax.out
@@ -0,0 +1,66 @@
+2%sint63
+     : int
+2
+     : int
+-3
+     : int
+4611686018427387903
+     : int
+-4611686018427387904
+     : int
+427
+     : int
+427
+     : int
+427
+     : int
+427
+     : int
+427
+     : int
+The command has indeed failed with message:
+Cannot interpret this number as a value of type int
+The command has indeed failed with message:
+Cannot interpret this number as a value of type int
+0
+     : int
+0
+     : int
+The command has indeed failed with message:
+The reference xg was not found in the current environment.
+The command has indeed failed with message:
+The reference xG was not found in the current environment.
+The command has indeed failed with message:
+The reference x1 was not found in the current environment.
+The command has indeed failed with message:
+The reference x was not found in the current environment.
+2 + 2
+     : int
+The command has indeed failed with message:
+Cannot interpret this number as a value of type int
+The command has indeed failed with message:
+Cannot interpret this number as a value of type int
+0x1%int63
+     : int
+0x7fffffffffffffff%int63
+     : int
+2
+     : nat
+2%sint63
+     : int
+t = 2%si63
+     : int
+t = 2%si63
+     : int
+2
+     : nat
+2
+     : int
+(2 + 2)%sint63
+     : int
+2 + 2
+     : int
+     = 4
+     : int
+     = 37151199385380486
+     : int
diff --git a/test-suite/output/Sint63Syntax.v b/test-suite/output/Sint63Syntax.v
new file mode 100644
index 0000000000..b9ed596537
--- /dev/null
+++ b/test-suite/output/Sint63Syntax.v
@@ -0,0 +1,49 @@
+Require Import Sint63.
+
+Check 2%sint63.
+Open Scope sint63_scope.
+Check 2.
+Check -3.
+Check 4611686018427387903.
+Check -4611686018427387904.
+Check 0x1ab.
+Check 0X1ab.
+Check 0x1Ab.
+Check 0x1aB.
+Check 0x1AB.
+Fail Check 0x1ap5.  (* exponents not implemented (yet?) *)
+Fail Check 0x1aP5.
+Check 0x0.
+Check 0x000.
+Fail Check 0xg.
+Fail Check 0xG.
+Fail Check 00x1.
+Fail Check 0x.
+Check (PrimInt63.add 2 2).
+Fail Check 4611686018427387904.
+Fail Check -4611686018427387905.
+
+Set Printing All.
+Check 1%sint63.
+Check (-1)%sint63.
+Unset Printing All.
+
+Open Scope nat_scope.
+Check 2. (* : nat *)
+Check 2%sint63.
+Delimit Scope sint63_scope with si63.
+Definition t := 2%sint63.
+Print t.
+Delimit Scope nat_scope with sint63.
+Print t.
+Check 2.
+Close Scope nat_scope.
+Check 2.
+Close Scope sint63_scope.
+Delimit Scope sint63_scope with sint63.
+
+Check (2 + 2)%sint63.
+Open Scope sint63_scope.
+Check (2+2).
+Eval vm_compute in 2+2.
+Eval vm_compute in 65675757 * 565675998.
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).