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.

9 files changed, 32 insertions, 3 deletions

diff --git a/theories/Compat/Coq88.v b/theories/Compat/Coq88.v
index 4142af05d2..578425bfb5 100644
--- a/theories/Compat/Coq88.v
+++ b/theories/Compat/Coq88.v
@@ -9,3 +9,17 @@
 (************************************************************************)
 
 (** Compatibility file for making Coq act similar to Coq v8.8 *)
+(** In Coq 8.9, prim token notations follow [Import] rather than
+    [Require].  So we make all of the relevant notations accessible in
+    compatibility mode. *)
+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.Int31.
+Declare ML Module "string_syntax_plugin".
+Declare ML Module "ascii_syntax_plugin".
+Declare ML Module "r_syntax_plugin".
+Declare ML Module "int31_syntax_plugin".
+Numeral Notation BinNums.Z BinIntDef.Z.of_int BinIntDef.Z.to_int : Z_scope.
+Numeral Notation BinNums.positive BinPosDef.Pos.of_int BinPosDef.Pos.to_int : positive_scope.
+Numeral Notation BinNums.N BinNatDef.N.of_int BinNatDef.N.to_int : N_scope.
diff --git a/theories/NArith/BinNat.v b/theories/NArith/BinNat.v
index 5d3ec5abc7..bd27f94abd 100644
--- a/theories/NArith/BinNat.v
+++ b/theories/NArith/BinNat.v
@@ -930,6 +930,8 @@ Bind Scope N_scope with N.t N.
 
 (** Exportation of notations *)
 
+Numeral Notation N N.of_uint N.to_uint : N_scope.
+
 Infix "+" := N.add : N_scope.
 Infix "-" := N.sub : N_scope.
 Infix "*" := N.mul : N_scope.
diff --git a/theories/NArith/BinNatDef.v b/theories/NArith/BinNatDef.v
index 8bbecf9acb..be12fffaaf 100644
--- a/theories/NArith/BinNatDef.v
+++ b/theories/NArith/BinNatDef.v
@@ -402,6 +402,9 @@ Definition to_uint n :=
 
 Definition to_int n := Decimal.Pos (to_uint n).
 
+Numeral Notation N of_uint to_uint : N_scope.
+
 End N.
 
+(** Re-export the notation for those who just [Import NatIntDef] *)
 Numeral Notation N N.of_uint N.to_uint : N_scope.
diff --git a/theories/Numbers/Cyclic/Int31/Cyclic31.v b/theories/Numbers/Cyclic/Int31/Cyclic31.v
index bd4f0279d4..ec480bb1eb 100644
--- a/theories/Numbers/Cyclic/Int31/Cyclic31.v
+++ b/theories/Numbers/Cyclic/Int31/Cyclic31.v
@@ -23,8 +23,6 @@ Require Import Zpow_facts.
 Require Import CyclicAxioms.
 Require Import ROmega.
 
-Declare ML Module "int31_syntax_plugin".
-
 Local Open Scope nat_scope.
 Local Open Scope int31_scope.
 
@@ -128,7 +126,7 @@ Section Basics.
 
  Lemma nshiftl_S_tail :
   forall n x, nshiftl x (S n) = nshiftl (shiftl x) n.
- Proof. 
+ Proof.
  intros n; elim n; simpl; intros; now f_equal.
  Qed.
 
diff --git a/theories/Numbers/Cyclic/Int31/Int31.v b/theories/Numbers/Cyclic/Int31/Int31.v
index 9f8da831d8..39af62c32f 100644
--- a/theories/Numbers/Cyclic/Int31/Int31.v
+++ b/theories/Numbers/Cyclic/Int31/Int31.v
@@ -15,6 +15,8 @@ Require Import Wf_nat.
 Require Export ZArith.
 Require Export DoubleType.
 
+Declare ML Module "int31_syntax_plugin".
+
 (** * 31-bit integers *)
 
 (** This file contains basic definitions of a 31-bit integer
diff --git a/theories/PArith/BinPos.v b/theories/PArith/BinPos.v
index 000d895e10..dcaae1606d 100644
--- a/theories/PArith/BinPos.v
+++ b/theories/PArith/BinPos.v
@@ -1871,6 +1871,8 @@ Bind Scope positive_scope with Pos.t positive.
 
 (** Exportation of notations *)
 
+Numeral Notation positive Pos.of_int Pos.to_uint : positive_scope.
+
 Infix "+" := Pos.add : positive_scope.
 Infix "-" := Pos.sub : positive_scope.
 Infix "*" := Pos.mul : positive_scope.
diff --git a/theories/PArith/BinPosDef.v b/theories/PArith/BinPosDef.v
index 39b609e9dd..7f30733559 100644
--- a/theories/PArith/BinPosDef.v
+++ b/theories/PArith/BinPosDef.v
@@ -616,6 +616,9 @@ Definition to_uint p := Decimal.rev (to_little_uint p).
 
 Definition to_int n := Decimal.Pos (to_uint n).
 
+Numeral Notation positive of_int to_uint : positive_scope.
+
 End Pos.
 
+(** Re-export the notation for those who just [Import BinPosDef] *)
 Numeral Notation positive Pos.of_int Pos.to_uint : positive_scope.
diff --git a/theories/ZArith/BinInt.v b/theories/ZArith/BinInt.v
index cf7397b57e..a11d491a8b 100644
--- a/theories/ZArith/BinInt.v
+++ b/theories/ZArith/BinInt.v
@@ -1248,6 +1248,8 @@ Bind Scope Z_scope with Z.t Z.
 
 (** Re-export Notations *)
 
+Numeral Notation Z Z.of_int Z.to_int : Z_scope.
+
 Infix "+" := Z.add : Z_scope.
 Notation "- x" := (Z.opp x) : Z_scope.
 Infix "-" := Z.sub : Z_scope.
diff --git a/theories/ZArith/BinIntDef.v b/theories/ZArith/BinIntDef.v
index 8abcd15700..8cb62622db 100644
--- a/theories/ZArith/BinIntDef.v
+++ b/theories/ZArith/BinIntDef.v
@@ -639,6 +639,9 @@ Definition lxor a b :=
    | neg a, neg b => of_N (N.lxor (Pos.pred_N a) (Pos.pred_N b))
  end.
 
+Numeral Notation Z of_int to_int : Z_scope.
+
 End Z.
 
+(** Re-export the notation for those who just [Import BinIntDef] *)
 Numeral Notation Z Z.of_int Z.to_int : Z_scope.