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.

13 files changed, 88 insertions, 4 deletions

diff --git a/CHANGES b/CHANGES
index b1f9d46ed8..5d1c9a9c2d 100644
--- a/CHANGES
+++ b/CHANGES
@@ -69,6 +69,24 @@ Standard Library
   `dec_int_scope` and `dec_uint_scope`, to clash less with ssreflect
   and other packages.  They are still delimited by `%int` and `%uint`.
 
+- Syntax notations for `string`, `ascii`, `Z`, `positive`, `N`, `R`,
+  and `int31` are no longer available merely by `Require`ing the files
+  that define the inductives.  You must `Import` `Coq.Strings.String`,
+  `Coq.Strings.Ascii`, `Coq.ZArith.BinIntDef`, `Coq.PArith.BinPosDef`,
+  `Coq.NArith.BinNatDef`, `Coq.Reals.Rdefinitions`, and
+  `Coq.Numbers.Cyclic.Int31.Int31`, respectively, to be able to use
+  these notations.  Note that passing `-compat 8.8` or issuing
+  `Require Import Coq.Compat.Coq88` will make these notations
+  available.  Users wishing to port their developments automatically
+  may download `fix.py` from
+  <https://gist.github.com/JasonGross/5d4558edf8f5c2c548a3d96c17820169>
+  and run a command like `while true; do make -Okj 2>&1 |
+  /path/to/fix.py; done` and get a cup of coffee.  (This command must
+  be manually interrupted once the build finishes all the way though.
+  Note also that this method is not fail-proof; you may have to adjust
+  some scopes if you were relying on string notations not being
+  available even when `string_scope` was open.)
+
 - Numeral syntax for `nat` is no longer available without loading the
   entire prelude (`Require Import Coq.Init.Prelude`).  This only
   impacts users running Coq without the init library (`-nois` or
diff --git a/interp/notation.ml b/interp/notation.ml
index 56d6acbdae..d6bd62e121 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -431,8 +431,8 @@ let subst_prim_token_interpretation (subs,infos) =
 
 let inPrimTokenInterp : prim_token_infos -> obj =
   declare_object {(default_object "PRIM-TOKEN-INTERP") with
+     open_function  = (fun i o -> if Int.equal i 1 then cache_prim_token_interpretation o);
      cache_function = cache_prim_token_interpretation;
-     load_function  = (fun _ -> cache_prim_token_interpretation);
      subst_function = subst_prim_token_interpretation;
      classify_function = (fun o -> Substitute o)}
 
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.
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.