Make Numeral Notation follow Import, not Require

Because that's the sane thing to do.

This will inevitably cause issues for projects which do not `Import
Coq.Strings.Ascii` before trying to use ascii notations.

We also move the syntax plugin for `int31` notations from `Cyclic31` to
`Int31`, so that users (like CompCert) who merely `Require Import
Coq.Numbers.Cyclic.Int31.Int31` get the `int31` numeral syntax.  Since
`Cyclic31` `Export`s `Int31`, this should not cause any additional
incompatibilities.

2 files changed, 37 insertions, 0 deletions

diff --git a/test-suite/success/Compat88.v b/test-suite/success/Compat88.v
new file mode 100644
index 0000000000..e2045900d5
--- /dev/null
+++ b/test-suite/success/Compat88.v
@@ -0,0 +1,18 @@
+(* -*- coq-prog-args: ("-compat" "8.8") -*- *)
+(** Check that various syntax usage is available without importing
+    relevant files. *)
+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 Import Coq.Compat.Coq88. (* XXX FIXME Should not need [Require], see https://github.com/coq/coq/issues/8311 *)
+
+Check String.String "a" String.EmptyString.
+Check String.eqb "a" "a".
+Check Nat.eqb 1 1.
+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.
diff --git a/test-suite/success/NumeralNotations.v b/test-suite/success/NumeralNotations.v
index 5a58a1b72d..bacc982ccc 100644
--- a/test-suite/success/NumeralNotations.v
+++ b/test-suite/success/NumeralNotations.v
@@ -228,3 +228,22 @@ Module Test13.
   Fail Numeral Notation unit of_uint to_uint'' : test13''_scope.
   Fail Check let v := 0%test13'' in v : unit.
 End Test13.
+
+Module Test14.
+  (* Test that numeral notations follow [Import], not [Require], and
+     also test for current (INCORRECT!!) behavior that [Local] has no
+     effect in modules. *)
+  Delimit Scope test14_scope with test14.
+  Delimit Scope test14'_scope with test14'.
+  Module Inner.
+    Definition to_uint (x : unit) : Decimal.uint := Nat.to_uint O.
+    Definition of_uint (x : Decimal.uint) : unit := tt.
+    Local Numeral Notation unit of_uint to_uint : test14_scope.
+    Global Numeral Notation unit of_uint to_uint : test14'_scope.
+  End Inner.
+  Fail Check let v := 0%test14 in v : unit.
+  Fail Check let v := 0%test14' in v : unit.
+  Import Inner.
+  Check let v := 0%test14 in v : unit. (* THIS SHOULD FAIL!! *)
+  Check let v := 0%test14' in v : unit.
+End Test14.