Merge PR #6914: Primitive integers

Ack-by: JasonGross
Ack-by: SkySkimmer
Ack-by: ejgallego
Ack-by: gares
Ack-by: maximedenes
Ack-by: ppedrot

40 files changed, 722 insertions, 9 deletions

diff --git a/test-suite/Makefile b/test-suite/Makefile
index cafc9a744c..68acb6f04d 100644
--- a/test-suite/Makefile
+++ b/test-suite/Makefile
@@ -95,7 +95,7 @@ INTERACTIVE := interactive
 UNIT_TESTS := unit-tests
 VSUBSYSTEMS := prerequisite success failure $(BUGS) output \
   output-modulo-time $(INTERACTIVE) micromega $(COMPLEXITY) modules stm \
-  coqdoc ssr
+  coqdoc ssr arithmetic
 
 # All subsystems
 SUBSYSTEMS := $(VSUBSYSTEMS) misc bugs ide vio coqchk coqwc coq-makefile tools $(UNIT_TESTS)
@@ -176,6 +176,7 @@ summary:
 	  $(call summary_dir, "Coqdoc tests", coqdoc); \
 	  $(call summary_dir, "tools/ tests", tools); \
 	  $(call summary_dir, "Unit tests", unit-tests); \
+	  $(call summary_dir, "Machine arithmetic tests", arithmetic); \
 	  nb_success=`find . -name '*.log' -exec tail -n2 '{}' \; | grep -e $(log_success) | wc -l`; \
 	  nb_failure=`find . -name '*.log' -exec tail -n2 '{}' \; | grep -e $(log_failure) | wc -l`; \
 	  nb_tests=`expr $$nb_success + $$nb_failure`; \
@@ -308,7 +309,7 @@ $(addsuffix .log,$(wildcard prerequisite/*.v)): %.v.log: %.v
 	$(HIDE)$(coqchk) -norec TestSuite.$(shell basename $< .v) > $(shell dirname $<)/$(shell basename $< .v).chk.log 2>&1
 
 ssr: $(wildcard ssr/*.v:%.v=%.v.log)
-$(addsuffix .log,$(wildcard ssr/*.v success/*.v micromega/*.v modules/*.v)): %.v.log: %.v $(PREREQUISITELOG)
+$(addsuffix .log,$(wildcard ssr/*.v success/*.v micromega/*.v modules/*.v arithmetic/*.v)): %.v.log: %.v $(PREREQUISITELOG)
 	@echo "TEST      $< $(call get_coq_prog_args_in_parens,"$<")"
 	$(HIDE){ \
 	  opts="$(if $(findstring modules/,$<),-R modules Mods)"; \
diff --git a/test-suite/arithmetic/add.v b/test-suite/arithmetic/add.v
new file mode 100644
index 0000000000..fb7eb1d53c
--- /dev/null
+++ b/test-suite/arithmetic/add.v
@@ -0,0 +1,18 @@
+Require Import Int63.
+
+Set Implicit Arguments.
+
+Open Scope int63_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 : 9223372036854775807 + 1 = 0).
+Check (eq_refl 0 <: 9223372036854775807 + 1 = 0).
+Check (eq_refl 0 <<: 9223372036854775807 + 1 = 0).
+Definition compute2 := Eval compute in 9223372036854775807 + 1.
+Check (eq_refl compute2 : 0 = 0).
diff --git a/test-suite/arithmetic/addc.v b/test-suite/arithmetic/addc.v
new file mode 100644
index 0000000000..432aec0291
--- /dev/null
+++ b/test-suite/arithmetic/addc.v
@@ -0,0 +1,17 @@
+Require Import Int63.
+
+Set Implicit Arguments.
+
+Open Scope int63_scope.
+
+Check (eq_refl : 2 +c 3 = C0 5).
+Check (eq_refl (C0 5) <: 2 +c 3 = C0 5).
+Check (eq_refl (C0 5) <<: 2 +c 3 = C0 5).
+Definition compute1 := Eval compute in 2 +c 3.
+Check (eq_refl compute1 : C0 5 = C0 5).
+
+Check (eq_refl : 9223372036854775807 +c 2 = C1 1).
+Check (eq_refl (C1 1) <: 9223372036854775807 +c 2 = C1 1).
+Check (eq_refl (C1 1) <<: 9223372036854775807 +c 2 = C1 1).
+Definition compute2 := Eval compute in 9223372036854775807 +c 2.
+Check (eq_refl compute2 : C1 1 = C1 1).
diff --git a/test-suite/arithmetic/addcarryc.v b/test-suite/arithmetic/addcarryc.v
new file mode 100644
index 0000000000..a4430769ca
--- /dev/null
+++ b/test-suite/arithmetic/addcarryc.v
@@ -0,0 +1,17 @@
+Require Import Int63.
+
+Set Implicit Arguments.
+
+Open Scope int63_scope.
+
+Check (eq_refl : addcarryc 2 3 = C0 6).
+Check (eq_refl (C0 6) <: addcarryc 2 3 = C0 6).
+Check (eq_refl (C0 6) <<: addcarryc 2 3 = C0 6).
+Definition compute1 := Eval compute in addcarryc 2 3.
+Check (eq_refl compute1 : C0 6 = C0 6).
+
+Check (eq_refl : addcarryc 9223372036854775807 2 = C1 2).
+Check (eq_refl (C1 2) <: addcarryc 9223372036854775807 2 = C1 2).
+Check (eq_refl (C1 2) <<: addcarryc 9223372036854775807 2 = C1 2).
+Definition compute2 := Eval compute in addcarryc 9223372036854775807 2.
+Check (eq_refl compute2 : C1 2 = C1 2).
diff --git a/test-suite/arithmetic/addmuldiv.v b/test-suite/arithmetic/addmuldiv.v
new file mode 100644
index 0000000000..72b0164b49
--- /dev/null
+++ b/test-suite/arithmetic/addmuldiv.v
@@ -0,0 +1,12 @@
+Require Import Int63.
+
+Set Implicit Arguments.
+
+Open Scope int63_scope.
+
+Check (eq_refl : addmuldiv 32 3 5629499534213120 = 12887523328).
+Check (eq_refl 12887523328 <: addmuldiv 32 3 5629499534213120 = 12887523328).
+Check (eq_refl 12887523328 <<: addmuldiv 32 3 5629499534213120 = 12887523328).
+
+Definition compute2 := Eval compute in addmuldiv 32 3 5629499534213120.
+Check (eq_refl compute2 : 12887523328 = 12887523328).
diff --git a/test-suite/arithmetic/compare.v b/test-suite/arithmetic/compare.v
new file mode 100644
index 0000000000..a8d1ea1226
--- /dev/null
+++ b/test-suite/arithmetic/compare.v
@@ -0,0 +1,23 @@
+Require Import Int63.
+
+Set Implicit Arguments.
+
+Open Scope int63_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 : 9223372036854775807 ?= 0 = Gt).
+Check (eq_refl Gt <: 9223372036854775807 ?= 0 = Gt).
+Check (eq_refl Gt <<: 9223372036854775807 ?= 0 = Gt).
+Definition compute3 := Eval compute in 9223372036854775807 ?= 0.
+Check (eq_refl compute3 : Gt = Gt).
diff --git a/test-suite/arithmetic/div.v b/test-suite/arithmetic/div.v
new file mode 100644
index 0000000000..0ee0b91580
--- /dev/null
+++ b/test-suite/arithmetic/div.v
@@ -0,0 +1,17 @@
+Require Import Int63.
+
+Set Implicit Arguments.
+
+Open Scope int63_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 : 3 / 2 = 1).
+Check (eq_refl 1 <: 3 / 2 = 1).
+Check (eq_refl 1 <<: 3 / 2 = 1).
+Definition compute2 := Eval compute in 3 / 2.
+Check (eq_refl compute2 : 1 = 1).
diff --git a/test-suite/arithmetic/diveucl.v b/test-suite/arithmetic/diveucl.v
new file mode 100644
index 0000000000..8f88a0f356
--- /dev/null
+++ b/test-suite/arithmetic/diveucl.v
@@ -0,0 +1,17 @@
+Require Import Int63.
+
+Set Implicit Arguments.
+
+Open Scope int63_scope.
+
+Check (eq_refl : diveucl 6 3 = (2,0)).
+Check (eq_refl (2,0) <: diveucl 6 3 = (2,0)).
+Check (eq_refl (2,0) <<: diveucl 6 3 = (2,0)).
+Definition compute1 := Eval compute in diveucl 6 3.
+Check (eq_refl compute1 : (2,0) = (2,0)).
+
+Check (eq_refl : diveucl 5 3 = (1,2)).
+Check (eq_refl (1,2) <: diveucl 5 3 = (1,2)).
+Check (eq_refl (1,2) <<: diveucl 5 3 = (1,2)).
+Definition compute2 := Eval compute in diveucl 5 3.
+Check (eq_refl compute2 : (1,2) = (1,2)).
diff --git a/test-suite/arithmetic/diveucl_21.v b/test-suite/arithmetic/diveucl_21.v
new file mode 100644
index 0000000000..7e12a08906
--- /dev/null
+++ b/test-suite/arithmetic/diveucl_21.v
@@ -0,0 +1,17 @@
+Require Import Int63.
+
+Set Implicit Arguments.
+
+Open Scope int63_scope.
+
+Check (eq_refl : diveucl_21 1 1 2 = (4611686018427387904,1)).
+Check (eq_refl (4611686018427387904,1) <: diveucl_21 1 1 2 = (4611686018427387904,1)).
+Check (eq_refl (4611686018427387904,1) <<: diveucl_21 1 1 2 = (4611686018427387904,1)).
+Definition compute1 := Eval compute in diveucl_21 1 1 2.
+Check (eq_refl compute1 : (4611686018427387904,1) = (4611686018427387904,1)).
+
+Check (eq_refl : diveucl_21 3 1 2 = (4611686018427387904, 1)).
+Check (eq_refl (4611686018427387904, 1) <: diveucl_21 3 1 2 = (4611686018427387904, 1)).
+Check (eq_refl (4611686018427387904, 1) <<: diveucl_21 3 1 2 = (4611686018427387904, 1)).
+Definition compute2 := Eval compute in diveucl_21 3 1 2.
+Check (eq_refl compute2 : (4611686018427387904, 1) = (4611686018427387904, 1)).
diff --git a/test-suite/arithmetic/eqb.v b/test-suite/arithmetic/eqb.v
new file mode 100644
index 0000000000..dcc0b71f6d
--- /dev/null
+++ b/test-suite/arithmetic/eqb.v
@@ -0,0 +1,17 @@
+Require Import Int63.
+
+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 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 compute2 : false = false).
diff --git a/test-suite/arithmetic/head0.v b/test-suite/arithmetic/head0.v
new file mode 100644
index 0000000000..f4234d2605
--- /dev/null
+++ b/test-suite/arithmetic/head0.v
@@ -0,0 +1,23 @@
+Require Import Int63.
+
+Set Implicit Arguments.
+
+Open Scope int63_scope.
+
+Check (eq_refl : head0 3 = 61).
+Check (eq_refl 61 <: head0 3 = 61).
+Check (eq_refl 61 <<: head0 3 = 61).
+Definition compute1 := Eval compute in head0 3.
+Check (eq_refl compute1 : 61 = 61).
+
+Check (eq_refl : head0 4611686018427387904 = 0).
+Check (eq_refl 0 <: head0 4611686018427387904 = 0).
+Check (eq_refl 0 <<: head0 4611686018427387904 = 0).
+Definition compute2 := Eval compute in head0 4611686018427387904.
+Check (eq_refl compute2 : 0 = 0).
+
+Check (eq_refl : head0 0 = 63).
+Check (eq_refl 63 <: head0 0 = 63).
+Check (eq_refl 63 <<: head0 0 = 63).
+Definition compute3 := Eval compute in head0 0.
+Check (eq_refl compute3 : 63 = 63).
diff --git a/test-suite/arithmetic/isint.v b/test-suite/arithmetic/isint.v
new file mode 100644
index 0000000000..c215caa878
--- /dev/null
+++ b/test-suite/arithmetic/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 Int63.
+
+Set Implicit Arguments.
+
+Open Scope int63_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/arithmetic/land.v b/test-suite/arithmetic/land.v
new file mode 100644
index 0000000000..0ea6fd90b6
--- /dev/null
+++ b/test-suite/arithmetic/land.v
@@ -0,0 +1,29 @@
+Require Import Int63.
+
+Set Implicit Arguments.
+
+Open Scope int63_scope.
+
+Check (eq_refl : 0 land 0 = 0).
+Check (eq_refl 0 <: 0 land 0 = 0).
+Check (eq_refl 0 <<: 0 land 0 = 0).
+Definition compute1 := Eval compute in 0 land 0.
+Check (eq_refl compute1 : 0 = 0).
+
+Check (eq_refl : 9223372036854775807 land 0 = 0).
+Check (eq_refl 0 <: 9223372036854775807 land 0 = 0).
+Check (eq_refl 0 <<: 9223372036854775807 land 0 = 0).
+Definition compute2 := Eval compute in 9223372036854775807 land 0.
+Check (eq_refl compute2 : 0 = 0).
+
+Check (eq_refl : 0 land 9223372036854775807 = 0).
+Check (eq_refl 0 <: 0 land 9223372036854775807 = 0).
+Check (eq_refl 0 <<: 0 land 9223372036854775807 = 0).
+Definition compute3 := Eval compute in 0 land 9223372036854775807.
+Check (eq_refl compute3 : 0 = 0).
+
+Check (eq_refl : 9223372036854775807 land 9223372036854775807 = 9223372036854775807).
+Check (eq_refl 9223372036854775807 <: 9223372036854775807 land 9223372036854775807 = 9223372036854775807).
+Check (eq_refl 9223372036854775807 <<: 9223372036854775807 land 9223372036854775807 = 9223372036854775807).
+Definition compute4 := Eval compute in 9223372036854775807 land 9223372036854775807.
+Check (eq_refl compute4 : 9223372036854775807 = 9223372036854775807).
diff --git a/test-suite/arithmetic/leb.v b/test-suite/arithmetic/leb.v
new file mode 100644
index 0000000000..5354919978
--- /dev/null
+++ b/test-suite/arithmetic/leb.v
@@ -0,0 +1,23 @@
+Require Import Int63.
+
+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 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 : 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/arithmetic/lor.v b/test-suite/arithmetic/lor.v
new file mode 100644
index 0000000000..9c3b85c054
--- /dev/null
+++ b/test-suite/arithmetic/lor.v
@@ -0,0 +1,29 @@
+Require Import Int63.
+
+Set Implicit Arguments.
+
+Open Scope int63_scope.
+
+Check (eq_refl : 0 lor 0 = 0).
+Check (eq_refl 0 <: 0 lor 0 = 0).
+Check (eq_refl 0 <<: 0 lor 0 = 0).
+Definition compute1 := Eval compute in 0 lor 0.
+Check (eq_refl compute1 : 0 = 0).
+
+Check (eq_refl : 9223372036854775807 lor 0 = 9223372036854775807).
+Check (eq_refl 9223372036854775807 <: 9223372036854775807 lor 0 = 9223372036854775807).
+Check (eq_refl 9223372036854775807 <<: 9223372036854775807 lor 0 = 9223372036854775807).
+Definition compute2 := Eval compute in 9223372036854775807 lor 0.
+Check (eq_refl compute2 : 9223372036854775807 = 9223372036854775807).
+
+Check (eq_refl : 0 lor 9223372036854775807 = 9223372036854775807).
+Check (eq_refl 9223372036854775807 <: 0 lor 9223372036854775807 = 9223372036854775807).
+Check (eq_refl 9223372036854775807 <<: 0 lor 9223372036854775807 = 9223372036854775807).
+Definition compute3 := Eval compute in 0 lor 9223372036854775807.
+Check (eq_refl compute3 : 9223372036854775807 = 9223372036854775807).
+
+Check (eq_refl : 9223372036854775807 lor 9223372036854775807 = 9223372036854775807).
+Check (eq_refl 9223372036854775807 <: 9223372036854775807 lor 9223372036854775807 = 9223372036854775807).
+Check (eq_refl 9223372036854775807 <<: 9223372036854775807 lor 9223372036854775807 = 9223372036854775807).
+Definition compute4 := Eval compute in 9223372036854775807 lor 9223372036854775807.
+Check (eq_refl compute4 : 9223372036854775807 = 9223372036854775807).
diff --git a/test-suite/arithmetic/lsl.v b/test-suite/arithmetic/lsl.v
new file mode 100644
index 0000000000..70f3b90140
--- /dev/null
+++ b/test-suite/arithmetic/lsl.v
@@ -0,0 +1,23 @@
+Require Import Int63.
+
+Set Implicit Arguments.
+
+Open Scope int63_scope.
+
+Check (eq_refl : 3 << 61 = 6917529027641081856).
+Check (eq_refl 6917529027641081856 <: 3 << 61 = 6917529027641081856).
+Check (eq_refl 6917529027641081856 <<: 3 << 61 = 6917529027641081856).
+Definition compute1 := Eval compute in 3 << 61.
+Check (eq_refl compute1 : 6917529027641081856 = 6917529027641081856).
+
+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 : 9223372036854775807 << 64 = 0).
+Check (eq_refl 0 <: 9223372036854775807 << 64 = 0).
+Check (eq_refl 0 <<: 9223372036854775807 << 64 = 0).
+Definition compute3 := Eval compute in 9223372036854775807 << 64.
+Check (eq_refl compute3 : 0 = 0).
diff --git a/test-suite/arithmetic/lsr.v b/test-suite/arithmetic/lsr.v
new file mode 100644
index 0000000000..c36c24e237
--- /dev/null
+++ b/test-suite/arithmetic/lsr.v
@@ -0,0 +1,23 @@
+Require Import Int63.
+
+Set Implicit Arguments.
+
+Open Scope int63_scope.
+
+Check (eq_refl : 6917529027641081856 >> 61 = 3).
+Check (eq_refl 3 <: 6917529027641081856 >> 61 = 3).
+Check (eq_refl 3 <<: 6917529027641081856 >> 61 = 3).
+Definition compute1 := Eval compute in 6917529027641081856 >> 61.
+Check (eq_refl compute1 : 3 = 3).
+
+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 : 9223372036854775807 >> 64 = 0).
+Check (eq_refl 0 <: 9223372036854775807 >> 64 = 0).
+Check (eq_refl 0 <<: 9223372036854775807 >> 64 = 0).
+Definition compute3 := Eval compute in 9223372036854775807 >> 64.
+Check (eq_refl compute3 : 0 = 0).
diff --git a/test-suite/arithmetic/ltb.v b/test-suite/arithmetic/ltb.v
new file mode 100644
index 0000000000..7ae5ac6493
--- /dev/null
+++ b/test-suite/arithmetic/ltb.v
@@ -0,0 +1,23 @@
+Require Import Int63.
+
+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 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 : 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/arithmetic/lxor.v b/test-suite/arithmetic/lxor.v
new file mode 100644
index 0000000000..b453fc7697
--- /dev/null
+++ b/test-suite/arithmetic/lxor.v
@@ -0,0 +1,29 @@
+Require Import Int63.
+
+Set Implicit Arguments.
+
+Open Scope int63_scope.
+
+Check (eq_refl : 0 lxor 0 = 0).
+Check (eq_refl 0 <: 0 lxor 0 = 0).
+Check (eq_refl 0 <<: 0 lxor 0 = 0).
+Definition compute1 := Eval compute in 0 lxor 0.
+Check (eq_refl compute1 : 0 = 0).
+
+Check (eq_refl : 9223372036854775807 lxor 0 = 9223372036854775807).
+Check (eq_refl 9223372036854775807 <: 9223372036854775807 lxor 0 = 9223372036854775807).
+Check (eq_refl 9223372036854775807 <<: 9223372036854775807 lxor 0 = 9223372036854775807).
+Definition compute2 := Eval compute in 9223372036854775807 lxor 0.
+Check (eq_refl compute2 : 9223372036854775807 = 9223372036854775807).
+
+Check (eq_refl : 0 lxor 9223372036854775807 = 9223372036854775807).
+Check (eq_refl 9223372036854775807 <: 0 lxor 9223372036854775807 = 9223372036854775807).
+Check (eq_refl 9223372036854775807 <<: 0 lxor 9223372036854775807 = 9223372036854775807).
+Definition compute3 := Eval compute in 0 lxor 9223372036854775807.
+Check (eq_refl compute3 : 9223372036854775807 = 9223372036854775807).
+
+Check (eq_refl : 9223372036854775807 lxor 9223372036854775807 = 0).
+Check (eq_refl 0 <: 9223372036854775807 lxor 9223372036854775807 = 0).
+Check (eq_refl 0 <<: 9223372036854775807 lxor 9223372036854775807 = 0).
+Definition compute4 := Eval compute in 9223372036854775807 lxor 9223372036854775807.
+Check (eq_refl compute4 : 0 = 0).
diff --git a/test-suite/arithmetic/mod.v b/test-suite/arithmetic/mod.v
new file mode 100644
index 0000000000..5307eed493
--- /dev/null
+++ b/test-suite/arithmetic/mod.v
@@ -0,0 +1,17 @@
+Require Import Int63.
+
+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 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 compute2 : 2 = 2).
diff --git a/test-suite/arithmetic/mul.v b/test-suite/arithmetic/mul.v
new file mode 100644
index 0000000000..9480e8cd46
--- /dev/null
+++ b/test-suite/arithmetic/mul.v
@@ -0,0 +1,17 @@
+Require Import Int63.
+
+Set Implicit Arguments.
+
+Open Scope int63_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 : 9223372036854775807 * 2 = 9223372036854775806).
+Check (eq_refl 9223372036854775806 <: 9223372036854775807 * 2 = 9223372036854775806).
+Check (eq_refl 9223372036854775806 <<: 9223372036854775807 * 2 = 9223372036854775806).
+Definition compute2 := Eval compute in 9223372036854775807 * 2.
+Check (eq_refl compute2 : 9223372036854775806 = 9223372036854775806).
diff --git a/test-suite/arithmetic/mulc.v b/test-suite/arithmetic/mulc.v
new file mode 100644
index 0000000000..e10855bafa
--- /dev/null
+++ b/test-suite/arithmetic/mulc.v
@@ -0,0 +1,22 @@
+Require Import Cyclic63.
+
+Set Implicit Arguments.
+
+Open Scope int63_scope.
+
+Check (eq_refl : 2 *c 3 = WW 0 6).
+Check (eq_refl (WW 0 6) <: 2 *c 3 = WW 0 6).
+Check (eq_refl (WW 0 6) <<: 2 *c 3 = WW 0 6).
+Definition compute1 := Eval compute in 2 *c 3.
+Check (eq_refl compute1 : WW 0 6 = WW 0 6).
+
+Check (eq_refl : 9223372036854775807 *c 2 = WW 1 9223372036854775806).
+Check (eq_refl (WW 1 9223372036854775806) <: 9223372036854775807 *c 2 = WW 1 9223372036854775806).
+Check (eq_refl (WW 1 9223372036854775806) <<: 9223372036854775807 *c 2 = WW 1 9223372036854775806).
+
+Definition compute2 := Eval compute in 9223372036854775807 *c 2.
+Check (eq_refl compute2 : WW 1 9223372036854775806 = WW 1 9223372036854775806).
+
+Check (eq_refl : 0 *c 0 = W0).
+Check (eq_refl (@W0 int) <: 0 *c 0 = W0).
+Check (eq_refl (@W0 int) <<: 0 *c 0 = W0).
diff --git a/test-suite/arithmetic/primitive.v b/test-suite/arithmetic/primitive.v
new file mode 100644
index 0000000000..f62f6109e1
--- /dev/null
+++ b/test-suite/arithmetic/primitive.v
@@ -0,0 +1,12 @@
+Section S.
+  Variable A : Type.
+  Fail Primitive int : let x := A in Set := #int63_type.
+  Fail Primitive add := #int63_add.
+End S.
+
+(* [Primitive] should be forbidden in sections, otherwise its type after cooking
+will be incorrect:
+
+Check int.
+
+*)
diff --git a/test-suite/arithmetic/reduction.v b/test-suite/arithmetic/reduction.v
new file mode 100644
index 0000000000..00e067ac5a
--- /dev/null
+++ b/test-suite/arithmetic/reduction.v
@@ -0,0 +1,28 @@
+Require Import Int63.
+
+Open Scope int63_scope.
+
+Definition div_eucl_plus_one i1 i2 :=
+  let (q,r) := diveucl i1 i2 in
+  (q+1, r+1)%int63.
+
+Definition rcbn := Eval cbn in div_eucl_plus_one 3 2.
+Check (eq_refl : rcbn = (2, 2)).
+
+Definition rcbv := Eval cbv in div_eucl_plus_one 3 2.
+Check (eq_refl : rcbv = (2, 2)).
+
+Definition rvmc := Eval vm_compute in div_eucl_plus_one 3 2.
+Check (eq_refl : rvmc = (2, 2)).
+
+Definition f n m :=
+  match (n ?= 42)%int63 with
+  | Lt => (n + m)%int63
+  | _ => (2*m)%int63
+  end.
+
+Goal forall n, (n ?= 42)%int63 = Gt -> f n 256 = 512%int63.
+  intros. unfold f.
+  cbn. Undo. cbv. (* Test reductions under match clauses *)
+  rewrite H. reflexivity.
+Qed.
diff --git a/test-suite/arithmetic/sub.v b/test-suite/arithmetic/sub.v
new file mode 100644
index 0000000000..1606fd2aa1
--- /dev/null
+++ b/test-suite/arithmetic/sub.v
@@ -0,0 +1,17 @@
+Require Import Int63.
+
+Set Implicit Arguments.
+
+Open Scope int63_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 = 9223372036854775807).
+Check (eq_refl 9223372036854775807 <: 0 - 1 = 9223372036854775807).
+Check (eq_refl 9223372036854775807 <<: 0 - 1 = 9223372036854775807).
+Definition compute2 := Eval compute in 0 - 1.
+Check (eq_refl compute2 : 9223372036854775807 = 9223372036854775807).
diff --git a/test-suite/arithmetic/subc.v b/test-suite/arithmetic/subc.v
new file mode 100644
index 0000000000..fc4067e48b
--- /dev/null
+++ b/test-suite/arithmetic/subc.v
@@ -0,0 +1,17 @@
+Require Import Int63.
+
+Set Implicit Arguments.
+
+Open Scope int63_scope.
+
+Check (eq_refl : 3 -c 2 = C0 1).
+Check (eq_refl (C0 1) <: 3 -c 2 = C0 1).
+Check (eq_refl (C0 1) <<: 3 -c 2 = C0 1).
+Definition compute1 := Eval compute in 3 -c 2.
+Check (eq_refl compute1 : C0 1 = C0 1).
+
+Check (eq_refl : 0 -c 1 = C1 9223372036854775807).
+Check (eq_refl (C1 9223372036854775807) <: 0 -c 1 = C1 9223372036854775807).
+Check (eq_refl (C1 9223372036854775807) <<: 0 -c 1 = C1 9223372036854775807).
+Definition compute2 := Eval compute in 0 -c 1.
+Check (eq_refl compute2 : C1 9223372036854775807 = C1 9223372036854775807).
diff --git a/test-suite/arithmetic/subcarryc.v b/test-suite/arithmetic/subcarryc.v
new file mode 100644
index 0000000000..e81b6536b2
--- /dev/null
+++ b/test-suite/arithmetic/subcarryc.v
@@ -0,0 +1,17 @@
+Require Import Int63.
+
+Set Implicit Arguments.
+
+Open Scope int63_scope.
+
+Check (eq_refl : subcarryc 3 1 = C0 1).
+Check (eq_refl (C0 1) <: subcarryc 3 1 = C0 1).
+Check (eq_refl (C0 1) <<: subcarryc 3 1 = C0 1).
+Definition compute1 := Eval compute in subcarryc 3 1.
+Check (eq_refl compute1 : C0 1 = C0 1).
+
+Check (eq_refl : subcarryc 0 1 = C1 9223372036854775806).
+Check (eq_refl (C1 9223372036854775806) <: subcarryc 0 1 = C1 9223372036854775806).
+Check (eq_refl (C1 9223372036854775806) <<: subcarryc 0 1 = C1 9223372036854775806).
+Definition compute2 := Eval compute in subcarryc 0 1.
+Check (eq_refl compute2 : C1 9223372036854775806 = C1 9223372036854775806).
diff --git a/test-suite/arithmetic/tail0.v b/test-suite/arithmetic/tail0.v
new file mode 100644
index 0000000000..c9d426087a
--- /dev/null
+++ b/test-suite/arithmetic/tail0.v
@@ -0,0 +1,23 @@
+Require Import Int63.
+
+Set Implicit Arguments.
+
+Open Scope int63_scope.
+
+Check (eq_refl : tail0 2305843009213693952 = 61).
+Check (eq_refl 61 <: tail0 2305843009213693952 = 61).
+Check (eq_refl 61 <<: tail0 2305843009213693952 = 61).
+Definition compute1 := Eval compute in tail0 2305843009213693952.
+Check (eq_refl compute1 : 61 = 61).
+
+Check (eq_refl : tail0 1 = 0).
+Check (eq_refl 0 <: tail0 1 = 0).
+Check (eq_refl 0 <<: tail0 1 = 0).
+Definition compute2 := Eval compute in tail0 1.
+Check (eq_refl compute2 : 0 = 0).
+
+Check (eq_refl : tail0 0 = 63).
+Check (eq_refl 63 <: tail0 0 = 63).
+Check (eq_refl 63 <<: tail0 0 = 63).
+Definition compute3 := Eval compute in tail0 0.
+Check (eq_refl compute3 : 63 = 63).
diff --git a/test-suite/arithmetic/unsigned.v b/test-suite/arithmetic/unsigned.v
new file mode 100644
index 0000000000..82920bd201
--- /dev/null
+++ b/test-suite/arithmetic/unsigned.v
@@ -0,0 +1,18 @@
+(* This file checks that operations over int63 are unsigned. *)
+Require Import Int63.
+
+Open Scope int63_scope.
+
+(* (0-1) must be the maximum integer value and not negative 1 *)
+
+Check (eq_refl : 1/(0-1) = 0).
+Check (eq_refl 0 <: 1/(0-1) = 0).
+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 compute2 : 3 = 3).
diff --git a/test-suite/failure/int31.v b/test-suite/failure/int63.v
index ed4c9f9c78..0bb87c6548 100644
--- a/test-suite/failure/int31.v
+++ b/test-suite/failure/int63.v
@@ -1,17 +1,16 @@
-Require Import Int31 Cyclic31.
+Require Import Int63 Cyclic63.
 
-Open Scope int31_scope.
+Open Scope int63_scope.
 
 (* This used to go through because of an unbalanced stack bug in the bytecode
 interpreter *)
 
 Lemma bad : False.
 assert (1 = 2).
-change 1 with (add31 (addmuldiv31 65 (add31 1 1) 2) 1).
+change 1 with (Int63.add (Int63.addmuldiv 129 (Int63.add 1 1) 2) 1).
 Fail vm_compute; reflexivity.
 (*
 discriminate.
 Qed.
 *)
 Abort.
-
diff --git a/test-suite/output/Int31Syntax.out b/test-suite/output/Int31Syntax.out
index 4e8796c14b..0d6504f5f8 100644
--- a/test-suite/output/Int31Syntax.out
+++ b/test-suite/output/Int31Syntax.out
@@ -12,3 +12,5 @@ I31
      : int31
      = 710436486
      : int31
+The command has indeed failed with message:
+Cannot interpret this number as a value of type int31
diff --git a/test-suite/output/Int31Syntax.v b/test-suite/output/Int31Syntax.v
index 83be3b976b..48889a26ef 100644
--- a/test-suite/output/Int31Syntax.v
+++ b/test-suite/output/Int31Syntax.v
@@ -3,11 +3,12 @@ Require Import Int31 Cyclic31.
 Open Scope int31_scope.
 Check I31. (* Would be nice to have I31 : digits->digits->...->int31
               For the moment, I31 : digits31 int31, which is better
-	      than (fix nfun .....) size int31 *)
+              than (fix nfun .....) size int31 *)
 Check 2.
 Check 1000000000000000000. (* = 660865024, after modulo 2^31 *)
 Check (add31 2 2).
 Check (2+2).
 Eval vm_compute in 2+2.
 Eval vm_compute in 65675757 * 565675998.
+Fail Check -1.
 Close Scope int31_scope.
diff --git a/test-suite/output/Int63Syntax.out b/test-suite/output/Int63Syntax.out
new file mode 100644
index 0000000000..fdd5599565
--- /dev/null
+++ b/test-suite/output/Int63Syntax.out
@@ -0,0 +1,16 @@
+2
+     : int
+9223372036854775807
+     : int
+2 + 2
+     : int
+2 + 2
+     : int
+     = 4
+     : int
+     = 37151199385380486
+     : int
+The command has indeed failed with message:
+int63 are only non-negative numbers.
+The command has indeed failed with message:
+overflow in int63 literal: 9223372036854775808
diff --git a/test-suite/output/Int63Syntax.v b/test-suite/output/Int63Syntax.v
new file mode 100644
index 0000000000..3dc364eddb
--- /dev/null
+++ b/test-suite/output/Int63Syntax.v
@@ -0,0 +1,12 @@
+Require Import Int63 Cyclic63.
+
+Open Scope int63_scope.
+Check 2.
+Check 9223372036854775807.
+Check (Int63.add 2 2).
+Check (2+2).
+Eval vm_compute in 2+2.
+Eval vm_compute in 65675757 * 565675998.
+Fail Check -1.
+Fail Check 9223372036854775808.
+Close Scope int63_scope.
diff --git a/test-suite/output/Notations4.out b/test-suite/output/Notations4.out
index 7a64b7eb45..efa895d709 100644
--- a/test-suite/output/Notations4.out
+++ b/test-suite/output/Notations4.out
@@ -51,3 +51,5 @@ r 2 3
      : Prop
 Notation Cn := Foo.FooCn
 Expands to: Notation Notations4.J.Mfoo.Foo.Bar.Cn
+let v := 0%test17 in v : myint63
+     : myint63
diff --git a/test-suite/output/Notations4.v b/test-suite/output/Notations4.v
index 90babf9c55..b4c65ce196 100644
--- a/test-suite/output/Notations4.v
+++ b/test-suite/output/Notations4.v
@@ -197,3 +197,16 @@ End Mfoo.
 About Cn.
 
 End J.
+
+Require Import Coq.Numbers.Cyclic.Int63.Int63.
+Module NumeralNotations.
+  Module Test17.
+    (** Test int63 *)
+    Declare Scope test17_scope.
+    Delimit Scope test17_scope with test17.
+    Local Set Primitive Projections.
+    Record myint63 := of_int { to_int : int }.
+    Numeral Notation myint63 of_int to_int : test17_scope.
+    Check let v := 0%test17 in v : myint63.
+  End Test17.
+End NumeralNotations.
diff --git a/test-suite/output/sint63Notation.out b/test-suite/output/sint63Notation.out
new file mode 100644
index 0000000000..9d325b38c7
--- /dev/null
+++ b/test-suite/output/sint63Notation.out
@@ -0,0 +1,24 @@
+     = 0
+     : uint
+     = 1
+     : uint
+     = 9223372036854775807
+     : uint
+let v := 0 in v : uint
+     : uint
+let v := 1 in v : uint
+     : uint
+let v := 9223372036854775807 in v : uint
+     : uint
+     = 0
+     : sint
+     = 1
+     : sint
+     = -1
+     : sint
+let v := 0 in v : sint
+     : sint
+let v := 1 in v : sint
+     : sint
+let v := -1 in v : sint
+     : sint
diff --git a/test-suite/output/sint63Notation.v b/test-suite/output/sint63Notation.v
new file mode 100644
index 0000000000..331d74ed3d
--- /dev/null
+++ b/test-suite/output/sint63Notation.v
@@ -0,0 +1,37 @@
+From Coq
+Require Import Int63.
+Import ZArith.
+
+Declare Scope uint_scope.
+Declare Scope sint_scope.
+Delimit Scope uint_scope with uint.
+Delimit Scope sint_scope with sint.
+
+Record uint := wrapu { unwrapu : int }.
+Record sint := wraps { unwraps : int }.
+
+Definition uof_Z (v : Z) := wrapu (of_Z v).
+Definition uto_Z (v : uint) := to_Z (unwrapu v).
+
+Definition sof_Z (v : Z) := wraps (of_Z (v mod (2 ^ 31))).
+Definition as_signed (bw : Z) (v : Z) :=
+  (((2 ^ (bw - 1) + v) mod (2 ^ bw)) - 2 ^ (bw - 1))%Z.
+
+Definition sto_Z (v : sint) := as_signed 31 (to_Z (unwraps v)).
+Numeral Notation uint uof_Z uto_Z : uint_scope.
+Numeral Notation sint sof_Z sto_Z : sint_scope.
+Open Scope uint_scope.
+Compute uof_Z 0.
+Compute uof_Z 1.
+Compute uof_Z (-1).
+Check let v := 0 in v : uint.
+Check let v := 1 in v : uint.
+Check let v := -1 in v : uint.
+Close Scope uint_scope.
+Open Scope sint_scope.
+Compute sof_Z 0.
+Compute sof_Z 1.
+Compute sof_Z (-1).
+Check let v := 0 in v : sint.
+Check let v := 1 in v : sint.
+Check let v := -1 in v : sint.
diff --git a/test-suite/success/Compat88.v b/test-suite/success/Compat88.v
index e2045900d5..1233a4b8f5 100644
--- a/test-suite/success/Compat88.v
+++ b/test-suite/success/Compat88.v
@@ -4,7 +4,7 @@
 Require Coq.Strings.Ascii Coq.Strings.String.
 Require Coq.ZArith.BinIntDef Coq.PArith.BinPosDef Coq.NArith.BinNatDef.
 Require Coq.Reals.Rdefinitions.
-Require Coq.Numbers.Cyclic.Int31.Cyclic31.
+Require Coq.Numbers.Cyclic.Int63.Cyclic63.
 
 Require Import Coq.Compat.Coq88. (* XXX FIXME Should not need [Require], see https://github.com/coq/coq/issues/8311 *)
 
@@ -15,4 +15,4 @@ Check BinNat.N.eqb 1 1.
 Check BinInt.Z.eqb 1 1.
 Check BinPos.Pos.eqb 1 1.
 Check Rdefinitions.Rplus 1 1.
-Check Int31.iszero 1.
+Check Int63.is_zero 1.
diff --git a/test-suite/success/NumeralNotations.v b/test-suite/success/NumeralNotations.v
index 47ef381270..7b857c70c5 100644
--- a/test-suite/success/NumeralNotations.v
+++ b/test-suite/success/NumeralNotations.v
@@ -300,3 +300,14 @@ Module Test16.
   (** Ideally this should work, but it should definitely not anomaly *)
   Fail Check let v := 0%test16 in v : Foo.
 End Test16.
+
+Require Import Coq.Numbers.Cyclic.Int63.Int63.
+Module Test17.
+  (** Test int63 *)
+  Declare Scope test17_scope.
+  Delimit Scope test17_scope with test17.
+  Local Set Primitive Projections.
+  Record myint63 := of_int { to_int : int }.
+  Numeral Notation myint63 of_int to_int : test17_scope.
+  Check let v := 0%test17 in v : myint63.
+End Test17.