Merge PR #6914: Primitive integers

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

2 files changed, 13 insertions, 2 deletions

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.