From b3c75936a4912ca794cdcecfeb92044552336c63 Mon Sep 17 00:00:00 2001
From: Pierre Letouzey
Date: Wed, 4 Apr 2018 10:43:38 +0200
Subject: prim notations backtrackable, their declarations now in two parts
 (API change)

 The first part (e.g. register_bignumeral_interpretation) deals only with
 the interp/uninterp closures. It should typically be done as a side
 effect during a syntax plugin loading. No prim notation are active yet
 after this phase.

 The second part (enable_prim_token_interpretation) activates the prim
 notation. It is now correctly talking to Summary and to the LibStack.
 To avoid "phantom" objects in libstack after a mere Require, this
 second part should be done inside a Mltop.declare_cache_obj

 The link between the two parts is a prim_token_uid (a string), which
 should be unique for each primitive notation. When this primitive
 notation is specific to a scope, the scope_name could be used as uid.

 Btw, the list of "patterns" for detecting when an uninterpreter should
 be considered is now restricted to a list of global_reference
 (inductive constructors, or injection functions such as IZR).
 The earlier API was accepting a glob_constr list, but was actually
 only working well for global_reference.

 A minimal compatibility is provided (declare_numeral_interpreter),
 but is discouraged, since it is known to store uncessary objects
 in the libstack.
---
 test-suite/interactive/PrimNotation.v | 18 ++++++++++++++++++
 1 file changed, 18 insertions(+)
 create mode 100644 test-suite/interactive/PrimNotation.v

(limited to 'test-suite')

diff --git a/test-suite/interactive/PrimNotation.v b/test-suite/interactive/PrimNotation.v
new file mode 100644
index 0000000000..ca8cba67d5
--- /dev/null
+++ b/test-suite/interactive/PrimNotation.v
@@ -0,0 +1,18 @@
+(* Until recently, the Notation.declare_numeral_notation wasn't synchronized
+   w.r.t. backtracking. This should be ok now.
+   This test is pretty artificial (we must declare Z_scope for this to work).
+*)
+
+Delimit Scope Z_scope with Z.
+Open Scope Z_scope.
+Check 0.
+(* 0 : nat *)
+Require BinNums.
+Check 0.
+(* 0 : BinNums.Z *)
+Back 2.
+Check 0.
+(* Expected answer: 0 : nat *)
+(* Used to fail with:
+Error: Cannot interpret in Z_scope without requiring first module BinNums.
+*)
-- 
cgit v1.2.3


From 377188d7bfd27518e6ab47d5017907b1f527a7dd Mon Sep 17 00:00:00 2001
From: Pierre Letouzey
Date: Mon, 12 Mar 2018 15:45:02 +0100
Subject: Numeral Notation + test-suite : fix 3 tests using Datatypes.v but not
 Prelude.v

 Earlier, the nat_syntax_plugin was loaded as soon as Datatypes.v.
 This would now implies to make Datatypes.v depends on Decimal.v.
 Instead, we postpone the Numeral Notation for nat until Prelude.v,
 and we adapt those three tests that happen to live strictly between
 Datatypes and Prelude.
---
 test-suite/bugs/closed/4527.v |  8 +++++---
 test-suite/bugs/closed/4533.v | 11 +++++++----
 test-suite/bugs/closed/4544.v |  3 ++-
 3 files changed, 14 insertions(+), 8 deletions(-)

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/4527.v b/test-suite/bugs/closed/4527.v
index 117d6523a8..f8cedfff6e 100644
--- a/test-suite/bugs/closed/4527.v
+++ b/test-suite/bugs/closed/4527.v
@@ -23,7 +23,9 @@ Module Export Datatypes.
 
 Set Implicit Arguments.
 Notation nat := Coq.Init.Datatypes.nat.
+Notation O := Coq.Init.Datatypes.O.
 Notation S := Coq.Init.Datatypes.S.
+Notation two := (S (S O)).
 
 Record prod (A B : Type) := pair { fst : A ; snd : B }.
 
@@ -159,7 +161,7 @@ End Adjointify.
            (n : nat) {A : Type@{i}} {B : Type@{j}}
            (f : A -> B) (C : B -> Type@{k}) : Type@{l}
     := match n with
-         | 0 => Unit@{l}
+         | O => Unit@{l}
          | S n => (forall (g : forall a, C (f a)),
                      ExtensionAlong@{i j k l l} f C g) *
                   forall (h k : forall b, C b),
@@ -220,12 +222,12 @@ Section ORecursion.
   Definition O_indpaths {P Q : Type} {Q_inO : In O Q}
              (g h : O P -> Q) (p : g o to O P == h o to O P)
   : g == h
-  := (fst (snd (extendable_to_O O 2) g h) p).1.
+  := (fst (snd (extendable_to_O O two) g h) p).1.
 
   Definition O_indpaths_beta {P Q : Type} {Q_inO : In O Q}
              (g h : O P -> Q) (p : g o (to O P) == h o (to O P)) (x : P)
   : O_indpaths g h p (to O P x) = p x
-  := (fst (snd (extendable_to_O O 2) g h) p).2 x.
+  := (fst (snd (extendable_to_O O two) g h) p).2 x.
 
 End ORecursion.
 
diff --git a/test-suite/bugs/closed/4533.v b/test-suite/bugs/closed/4533.v
index c3e0da1117..fd2380a070 100644
--- a/test-suite/bugs/closed/4533.v
+++ b/test-suite/bugs/closed/4533.v
@@ -17,7 +17,10 @@ Notation "A -> B" := (forall (_ : A), B) : type_scope.
 Module Export Datatypes.
   Set Implicit Arguments.
   Notation nat := Coq.Init.Datatypes.nat.
+  Notation O := Coq.Init.Datatypes.O.
   Notation S := Coq.Init.Datatypes.S.
+  Notation one := (S O).
+  Notation two := (S one).
   Record prod (A B : Type) := pair { fst : A ; snd : B }.
   Notation "x * y" := (prod x y) : type_scope.
   Delimit Scope nat_scope with nat.
@@ -109,7 +112,7 @@ Fixpoint ExtendableAlong@{i j k l}
          (n : nat) {A : Type@{i}} {B : Type@{j}}
          (f : A -> B) (C : B -> Type@{k}) : Type@{l}
   := match n with
-     | 0 => Unit@{l}
+     | O => Unit@{l}
      | S n => (forall (g : forall a, C (f a)),
                   ExtensionAlong@{i j k l l} f C g) *
               forall (h k : forall b, C b),
@@ -160,17 +163,17 @@ Module ReflectiveSubuniverses_Theory (Os : ReflectiveSubuniverses).
     Definition O_rec {P Q : Type} {Q_inO : In O Q}
                (f : P -> Q)
       : O P -> Q
-      := (fst (extendable_to_O O 1%nat) f).1.
+      := (fst (extendable_to_O O one) f).1.
 
     Definition O_rec_beta {P Q : Type} {Q_inO : In O Q}
                (f : P -> Q) (x : P)
       : O_rec f (to O P x) = f x
-      := (fst (extendable_to_O O 1%nat) f).2 x.
+      := (fst (extendable_to_O O one) f).2 x.
 
     Definition O_indpaths {P Q : Type} {Q_inO : In O Q}
                (g h : O P -> Q) (p : g o to O P == h o to O P)
       : g == h
-      := (fst (snd (extendable_to_O O 2) g h) p).1.
+      := (fst (snd (extendable_to_O O two) g h) p).1.
 
   End ORecursion.
 
diff --git a/test-suite/bugs/closed/4544.v b/test-suite/bugs/closed/4544.v
index 4ad53bc629..13c47edc8f 100644
--- a/test-suite/bugs/closed/4544.v
+++ b/test-suite/bugs/closed/4544.v
@@ -19,6 +19,7 @@ Inductive sum (A B : Type) : Type :=
   | inl : A -> sum A B
   | inr : B -> sum A B.
 Notation nat := Coq.Init.Datatypes.nat.
+Notation O := Coq.Init.Datatypes.O.
 Notation S := Coq.Init.Datatypes.S.
 Notation "x + y" := (sum x y) : type_scope.
 
@@ -449,7 +450,7 @@ Section Extensions.
            (n : nat) {A : Type@{i}} {B : Type@{j}}
            (f : A -> B) (C : B -> Type@{k}) : Type@{l}
     := match n with
-         | 0 => Unit@{l}
+         | O => Unit@{l}
          | S n => (forall (g : forall a, C (f a)),
                      ExtensionAlong@{i j k l l} f C g) *
                   forall (h k : forall b, C b),
-- 
cgit v1.2.3


From 3c7c0bb08d406d4addfc0ac68dce45bf7c5cb7e9 Mon Sep 17 00:00:00 2001
From: Pierre Letouzey
Date: Wed, 11 Apr 2018 09:58:56 +0200
Subject: WIP: adapt Numeral Notation to synchronized prim notations

---
 test-suite/interactive/PrimNotation.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'test-suite')

diff --git a/test-suite/interactive/PrimNotation.v b/test-suite/interactive/PrimNotation.v
index ca8cba67d5..4c81095c68 100644
--- a/test-suite/interactive/PrimNotation.v
+++ b/test-suite/interactive/PrimNotation.v
@@ -7,7 +7,7 @@ Delimit Scope Z_scope with Z.
 Open Scope Z_scope.
 Check 0.
 (* 0 : nat *)
-Require BinNums.
+Require BinInt.
 Check 0.
 (* 0 : BinNums.Z *)
 Back 2.
-- 
cgit v1.2.3


From fa0f378c91286d9127777a06b1dc557f695c22ae Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Sat, 14 Jul 2018 06:25:22 -0400
Subject: Fix numeral notation for a rebase on top of master

Some of this code is cargo-culted or kludged to work.

As I understand it, the situation is as follows:
There are two sorts of use-cases that need to be supported:
1. A plugin registers an OCaml function as a numeral interpreter.  In
   this case, the function registration must be synchronized with the
   document state, but the functions should not be marshelled / stored
   in the .vo.
2. A vernacular registers a Gallina function as a numeral interpreter.
   In this case, the registration must be synchronized, and the function
   should be marshelled / stored in the .vo.

In case (1), we can compare functions by pointer equality, and we should
be able to rely on globally unique keys, even across backtracking.

In case (2), we cannot compare functions by pointer equality (because
they must be regenerated on unmarshelling when `Require`ing a .vo file),
and we also cannot rely on any sort of unique key being both unique and
persistent across files.

The solution we use here is that we ask clients to provide "unique"
keys, and that clients tell us whether or not to overwrite existing
registered functions, i.e., to tell us whether or not we should expect
interpreter functions to be globally unique under pointer equality.  For
plugins, a simple string suffices, as long as the string does not clash
between different plugins.  In the case of vernacular-registered
functions, use marshell a description of all of the data used to
generate the function, and use that string as a unique key which is
expected to persist across files.  Because we cannot rely on
function-pointer uniqueness here, we tell the
interpretation-registration to allow overwriting.

----

Some of this code is response to comments on the PR

----

Some code is to fix an issue that bignums revealed:

Both Int31 and bignums registered numeral notations in int31_scope.  We
now prepend a globally unique identifier when registering numeral
notations from OCaml plugins.  This is permissible because we don't
store the uid information for such notations in .vo files (assuming I'm
understanding the code correctly).
---
 test-suite/success/NumeralNotations.v | 55 +++++++++++++++++++++++++++++++++++
 1 file changed, 55 insertions(+)
 create mode 100644 test-suite/success/NumeralNotations.v

(limited to 'test-suite')

diff --git a/test-suite/success/NumeralNotations.v b/test-suite/success/NumeralNotations.v
new file mode 100644
index 0000000000..a06327c5e6
--- /dev/null
+++ b/test-suite/success/NumeralNotations.v
@@ -0,0 +1,55 @@
+
+(* Test that we fail, rather than raising anomalies, on opaque terms during interpretation *)
+
+(* https://github.com/coq/coq/pull/8064#discussion_r202497516 *)
+Module Test1.
+  Axiom hold : forall {A B C}, A -> B -> C.
+  Definition opaque3 (x : Decimal.int) : Decimal.int := hold x (fix f (x : nat) : nat := match x with O => O | S n => S (f n) end).
+  Numeral Notation Decimal.int opaque3 opaque3 : opaque_scope.
+  Delimit Scope opaque_scope with opaque.
+  Fail Check 1%opaque.
+End Test1.
+
+(* https://github.com/coq/coq/pull/8064#discussion_r202497990 *)
+Module Test2.
+  Axiom opaque4 : option Decimal.int.
+  Definition opaque6 (x : Decimal.int) : option Decimal.int := opaque4.
+  Numeral Notation Decimal.int opaque6 opaque6 : opaque_scope.
+  Delimit Scope opaque_scope with opaque.
+  Open Scope opaque_scope.
+  Fail Check 1%opaque.
+End Test2.
+
+Module Test3.
+  Inductive silly := SILLY (v : Decimal.uint) (f : forall A, A -> A).
+  Definition to_silly (v : Decimal.uint) := SILLY v (fun _ x => x).
+  Definition of_silly (v : silly) := match v with SILLY v _ => v end.
+  Numeral Notation silly to_silly of_silly : silly_scope.
+  Delimit Scope silly_scope with silly.
+  Fail Check 1%silly.
+End Test3.
+
+
+Module Test4.
+  Polymorphic Inductive punit := ptt.
+  Polymorphic Definition pto_punit (v : Decimal.uint) : option punit := match Nat.of_uint v with O => Some ptt | _ => None end.
+  Polymorphic Definition pof_punit (v : punit) : Decimal.uint := Nat.to_uint 0.
+  Definition to_punit (v : Decimal.uint) : option punit := match Nat.of_uint v with O => Some ptt | _ => None end.
+  Definition of_punit (v : punit) : Decimal.uint := Nat.to_uint 0.
+  Polymorphic Definition pto_unit (v : Decimal.uint) : option unit := match Nat.of_uint v with O => Some tt | _ => None end.
+  Polymorphic Definition pof_unit (v : unit) : Decimal.uint := Nat.to_uint 0.
+  Definition to_unit (v : Decimal.uint) : option unit := match Nat.of_uint v with O => Some tt | _ => None end.
+  Definition of_unit (v : unit) : Decimal.uint := Nat.to_uint 0.
+  Fail Numeral Notation punit to_punit of_punit : pto.
+  Fail Numeral Notation punit pto_punit of_punit : ppo.
+  Fail Numeral Notation punit to_punit pof_punit : ptp.
+  Fail Numeral Notation punit pto_punit pof_punit : ppp.
+  Numeral Notation unit to_unit of_unit : uto.
+  Delimit Scope uto with uto.
+  Check let v := 0%uto in v : unit.
+  Fail Check 1%uto.
+  Fail Check (-1)%uto.
+  Fail Numeral Notation unit pto_unit of_unit : upo.
+  Fail Numeral Notation unit to_unit pof_unit : utp.
+  Fail Numeral Notation unit pto_unit pof_unit : upp.
+End Test4.
-- 
cgit v1.2.3


From ebf453d4ae4e4f0312f3fd696da26c03671bc906 Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Tue, 24 Jul 2018 13:06:03 -0400
Subject: Update doc and test-suite after supporting univ poly

Also make `Check S` no longer anomaly

Add a couple more test cases for numeral notations

Also add another possibly-confusing error message to the doc.

Respond to Hugo's doc request with Zimmi48's suggestion

From https://github.com/coq/coq/pull/8064/files#r204191608
---
 test-suite/interactive/PrimNotation.v |  58 ++++++++++++++--
 test-suite/success/NumeralNotations.v | 123 +++++++++++++++++++++++++++++++---
 2 files changed, 167 insertions(+), 14 deletions(-)

(limited to 'test-suite')

diff --git a/test-suite/interactive/PrimNotation.v b/test-suite/interactive/PrimNotation.v
index 4c81095c68..07986b0df3 100644
--- a/test-suite/interactive/PrimNotation.v
+++ b/test-suite/interactive/PrimNotation.v
@@ -5,14 +5,60 @@
 
 Delimit Scope Z_scope with Z.
 Open Scope Z_scope.
-Check 0.
-(* 0 : nat *)
+Check let v := 0 in v : nat.
+(* let v := 0 in v : nat : nat *)
 Require BinInt.
-Check 0.
-(* 0 : BinNums.Z *)
+Check let v := 0 in v : BinNums.Z.
+(* let v := 0 in v : BinNums.Z : BinNums.Z *)
 Back 2.
-Check 0.
-(* Expected answer: 0 : nat *)
+Check let v := 0 in v : nat.
+(* Expected answer: let v := 0 in v : nat : nat *)
 (* Used to fail with:
 Error: Cannot interpret in Z_scope without requiring first module BinNums.
 *)
+
+Local Set Universe Polymorphism.
+Delimit Scope punit_scope with punit.
+Delimit Scope pcunit_scope with pcunit.
+Delimit Scope int_scope with int.
+Numeral Notation Decimal.int Decimal.int_of_int Decimal.int_of_int : int_scope.
+Module A.
+  NonCumulative Inductive punit@{u} : Type@{u} := ptt.
+  Cumulative Inductive pcunit@{u} : Type@{u} := pctt.
+  Definition to_punit : Decimal.int -> option punit
+    := fun v => match v with 0%int => Some ptt | _ => None end.
+  Definition to_pcunit : Decimal.int -> option pcunit
+    := fun v => match v with 0%int => Some pctt | _ => None end.
+  Definition of_punit : punit -> Decimal.uint := fun _ => Nat.to_uint 0.
+  Definition of_pcunit : pcunit -> Decimal.uint := fun _ => Nat.to_uint 0.
+  Numeral Notation punit to_punit of_punit : punit_scope.
+  Check let v := 0%punit in v : punit.
+  Back 2.
+  Numeral Notation pcunit to_pcunit of_pcunit : punit_scope.
+  Check let v := 0%punit in v : pcunit.
+End A.
+Reset A.
+Local Unset Universe Polymorphism.
+Module A.
+  Inductive punit : Set := ptt.
+  Definition to_punit : Decimal.int -> option punit
+    := fun v => match v with 0%int => Some ptt | _ => None end.
+  Definition of_punit : punit -> Decimal.uint := fun _ => Nat.to_uint 0.
+  Numeral Notation punit to_punit of_punit : punit_scope.
+  Check let v := 0%punit in v : punit.
+End A.
+Local Set Universe Polymorphism.
+Inductive punit@{u} : Type@{u} := ptt.
+Definition to_punit : Decimal.int -> option punit
+  := fun v => match v with 0%int => Some ptt | _ => None end.
+Definition of_punit : punit -> Decimal.uint := fun _ => Nat.to_uint 0.
+Numeral Notation punit to_punit of_punit : punit_scope.
+Check let v := 0%punit in v : punit.
+Back 6. (* check backtracking of registering universe polymorphic constants *)
+Local Unset Universe Polymorphism.
+Inductive punit : Set := ptt.
+Definition to_punit : Decimal.int -> option punit
+  := fun v => match v with 0%int => Some ptt | _ => None end.
+Definition of_punit : punit -> Decimal.uint := fun _ => Nat.to_uint 0.
+Numeral Notation punit to_punit of_punit : punit_scope.
+Check let v := 0%punit in v : punit.
diff --git a/test-suite/success/NumeralNotations.v b/test-suite/success/NumeralNotations.v
index a06327c5e6..907ec32671 100644
--- a/test-suite/success/NumeralNotations.v
+++ b/test-suite/success/NumeralNotations.v
@@ -31,8 +31,9 @@ End Test3.
 
 
 Module Test4.
-  Polymorphic Inductive punit := ptt.
+  Polymorphic NonCumulative Inductive punit := ptt.
   Polymorphic Definition pto_punit (v : Decimal.uint) : option punit := match Nat.of_uint v with O => Some ptt | _ => None end.
+  Polymorphic Definition pto_punit_all (v : Decimal.uint) : punit := ptt.
   Polymorphic Definition pof_punit (v : punit) : Decimal.uint := Nat.to_uint 0.
   Definition to_punit (v : Decimal.uint) : option punit := match Nat.of_uint v with O => Some ptt | _ => None end.
   Definition of_punit (v : punit) : Decimal.uint := Nat.to_uint 0.
@@ -40,16 +41,122 @@ Module Test4.
   Polymorphic Definition pof_unit (v : unit) : Decimal.uint := Nat.to_uint 0.
   Definition to_unit (v : Decimal.uint) : option unit := match Nat.of_uint v with O => Some tt | _ => None end.
   Definition of_unit (v : unit) : Decimal.uint := Nat.to_uint 0.
-  Fail Numeral Notation punit to_punit of_punit : pto.
-  Fail Numeral Notation punit pto_punit of_punit : ppo.
-  Fail Numeral Notation punit to_punit pof_punit : ptp.
-  Fail Numeral Notation punit pto_punit pof_punit : ppp.
+  Numeral Notation punit to_punit of_punit : pto.
+  Numeral Notation punit pto_punit of_punit : ppo.
+  Numeral Notation punit to_punit pof_punit : ptp.
+  Numeral Notation punit pto_punit pof_punit : ppp.
   Numeral Notation unit to_unit of_unit : uto.
+  Delimit Scope pto with pto.
+  Delimit Scope ppo with ppo.
+  Delimit Scope ptp with ptp.
+  Delimit Scope ppp with ppp.
   Delimit Scope uto with uto.
+  Check let v := 0%pto in v : punit.
+  Check let v := 0%ppo in v : punit.
+  Check let v := 0%ptp in v : punit.
+  Check let v := 0%ppp in v : punit.
   Check let v := 0%uto in v : unit.
   Fail Check 1%uto.
   Fail Check (-1)%uto.
-  Fail Numeral Notation unit pto_unit of_unit : upo.
-  Fail Numeral Notation unit to_unit pof_unit : utp.
-  Fail Numeral Notation unit pto_unit pof_unit : upp.
+  Numeral Notation unit pto_unit of_unit : upo.
+  Numeral Notation unit to_unit pof_unit : utp.
+  Numeral Notation unit pto_unit pof_unit : upp.
+  Delimit Scope upo with upo.
+  Delimit Scope utp with utp.
+  Delimit Scope upp with upp.
+  Check let v := 0%upo in v : unit.
+  Check let v := 0%utp in v : unit.
+  Check let v := 0%upp in v : unit.
+
+  Polymorphic Definition pto_punits := pto_punit_all@{Set}.
+  Polymorphic Definition pof_punits := pof_punit@{Set}.
+  Numeral Notation punit pto_punits pof_punits : ppps (abstract after 1).
+  Delimit Scope ppps with ppps.
+  Universe u.
+  Constraint Set < u.
+  Check let v := 0%ppps in v : punit@{u}. (* Check that universes are refreshed *)
+  Fail Check let v := 1%ppps in v : punit@{u}. (* Note that universes are not refreshed here *)
 End Test4.
+
+Module Test5.
+  Check S. (* At one point gave Error: Anomaly "Uncaught exception Pretype_errors.PretypeError(_, _, _)." Please report at http://coq.inria.fr/bugs/. *)
+End Test5.
+
+Module Test6.
+  (* Check that numeral notations on enormous terms don't take forever to print/parse *)
+  (* Ackerman definition from https://stackoverflow.com/a/10303475/377022 *)
+  Fixpoint ack (n m : nat) : nat :=
+    match n with
+    | O => S m
+    | S p => let fix ackn (m : nat) :=
+                 match m with
+                 | O => ack p 1
+                 | S q => ack p (ackn q)
+                 end
+             in ackn m
+    end.
+
+  Timeout 1 Check (S (ack 4 4)). (* should be instantaneous *)
+
+  Local Set Primitive Projections.
+  Record > wnat := wrap { unwrap :> nat }.
+  Definition to_uint (x : wnat) : Decimal.uint := Nat.to_uint x.
+  Definition of_uint (x : Decimal.uint) : wnat := Nat.of_uint x.
+  Module Export Scopes.
+    Delimit Scope wnat_scope with wnat.
+  End Scopes.
+  Module Export Notations.
+    Export Scopes.
+    Numeral Notation wnat of_uint to_uint : wnat_scope (abstract after 5000).
+  End Notations.
+  Check let v := 0%wnat in v : wnat.
+  Check wrap O.
+  Timeout 1 Check wrap (ack 4 4). (* should be instantaneous *)
+End Test6.
+
+Module Test6_2.
+  Import Test6.Scopes.
+  Check Test6.wrap 0.
+  Import Test6.Notations.
+  Check let v := 0%wnat in v : Test6.wnat.
+End Test6_2.
+
+Module Test7.
+  Local Set Primitive Projections.
+  Record > wuint := wrap { unwrap : Decimal.uint }.
+  Delimit Scope wuint_scope with wuint.
+  Fail Numeral Notation wuint wrap unwrap : wuint_scope.
+End Test7.
+
+Module Test8.
+  Local Set Primitive Projections.
+  Record > wuint := wrap { unwrap : Decimal.uint }.
+  Delimit Scope wuint_scope with wuint.
+  Section with_var.
+    Context (dummy : unit).
+    Definition wrap' := let __ := dummy in wrap.
+    Definition unwrap' := let __ := dummy in unwrap.
+    Global Numeral Notation wuint wrap' unwrap' : wuint_scope.
+    Check let v := 0%wuint in v : wuint.
+  End with_var.
+  Fail Check let v := 0%wuint in v : wuint.
+  Compute wrap (Nat.to_uint 0).
+
+  Notation wrap'' := wrap.
+  Notation unwrap'' := unwrap.
+  Fail Numeral Notation wuint wrap'' unwrap'' : wuint_scope.
+End Test8.
+
+Module Test9.
+  Section with_let.
+    Local Set Primitive Projections.
+    Record > wuint := wrap { unwrap : Decimal.uint }.
+    Let wrap' := wrap.
+    Let unwrap' := unwrap.
+    Local Notation wrap'' := wrap.
+    Local Notation unwrap'' := unwrap.
+    Delimit Scope wuint_scope with wuint.
+    Fail Numeral Notation wuint wrap' unwrap' : wuint_scope.
+    Fail Numeral Notation wuint wrap'' unwrap'' : wuint_scope.
+  End with_let.
+End Test9.
-- 
cgit v1.2.3


From 296ac045fdfe6d6ae4875d7a6c89cad0c64c2e97 Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Tue, 14 Aug 2018 11:25:19 -0400
Subject: Add a warning about abstract after being a no-op

As per https://github.com/coq/coq/pull/8064#discussion_r209875616

I decided to make it a warning because it seems more flexible that way;
users to are flipping back and forth between option types and not option
types while designing won't have to update their `abstract after`
directives to do so, and users who don't want to allow this can make it an
actual error message.
---
 test-suite/success/NumeralNotations.v | 15 +++++++++++++++
 1 file changed, 15 insertions(+)

(limited to 'test-suite')

diff --git a/test-suite/success/NumeralNotations.v b/test-suite/success/NumeralNotations.v
index 907ec32671..2072fbbf62 100644
--- a/test-suite/success/NumeralNotations.v
+++ b/test-suite/success/NumeralNotations.v
@@ -160,3 +160,18 @@ Module Test9.
     Fail Numeral Notation wuint wrap'' unwrap'' : wuint_scope.
   End with_let.
 End Test9.
+
+Module Test10.
+  (* Test that it is only a warning to add abstract after to an optional parsing function *)
+  Definition to_uint (v : unit) := Nat.to_uint 0.
+  Definition of_uint (v : Decimal.uint) := match Nat.of_uint v with O => Some tt | _ => None end.
+  Definition of_any_uint (v : Decimal.uint) := tt.
+  Delimit Scope unit_scope with unit.
+  Delimit Scope unit2_scope with unit2.
+  Numeral Notation unit of_uint to_uint : unit_scope (abstract after 1).
+  Local Set Warnings Append "+abstract-large-number-no-op".
+  (* Check that there is actually a warning here *)
+  Fail Numeral Notation unit of_uint to_uint : unit2_scope (abstract after 1).
+  (* Check that there is no warning here *)
+  Numeral Notation unit of_any_uint to_uint : unit2_scope (abstract after 1).
+End Test10.
-- 
cgit v1.2.3


From 14626ba6a27323ac5a329c9f246bf64282738e5e Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Wed, 15 Aug 2018 11:03:42 -0400
Subject: Add Numeral Notation GlobRef printing/parsing

Now we support using inductive constructors and section-local variables
as numeral notation printing and parsing functions.

I'm not sure that I got the econstr conversion right.
---
 test-suite/success/NumeralNotations.v | 48 ++++++++++++++++++++++++++---------
 1 file changed, 36 insertions(+), 12 deletions(-)

(limited to 'test-suite')

diff --git a/test-suite/success/NumeralNotations.v b/test-suite/success/NumeralNotations.v
index 2072fbbf62..e63b9dc4c7 100644
--- a/test-suite/success/NumeralNotations.v
+++ b/test-suite/success/NumeralNotations.v
@@ -123,42 +123,52 @@ End Test6_2.
 
 Module Test7.
   Local Set Primitive Projections.
-  Record > wuint := wrap { unwrap : Decimal.uint }.
+  Record wuint := wrap { unwrap : Decimal.uint }.
   Delimit Scope wuint_scope with wuint.
-  Fail Numeral Notation wuint wrap unwrap : wuint_scope.
+  Numeral Notation wuint wrap unwrap : wuint_scope.
+  Check let v := 0%wuint in v : wuint.
+  Check let v := 1%wuint in v : wuint.
 End Test7.
 
 Module Test8.
   Local Set Primitive Projections.
-  Record > wuint := wrap { unwrap : Decimal.uint }.
-  Delimit Scope wuint_scope with wuint.
+  Record wuint := wrap { unwrap : Decimal.uint }.
+  Delimit Scope wuint8_scope with wuint8.
+  Delimit Scope wuint8'_scope with wuint8'.
   Section with_var.
     Context (dummy : unit).
     Definition wrap' := let __ := dummy in wrap.
     Definition unwrap' := let __ := dummy in unwrap.
-    Global Numeral Notation wuint wrap' unwrap' : wuint_scope.
-    Check let v := 0%wuint in v : wuint.
+    Global Numeral Notation wuint wrap' unwrap' : wuint8_scope.
+    Check let v := 0%wuint8 in v : wuint.
   End with_var.
-  Fail Check let v := 0%wuint in v : wuint.
+  Check let v := 0%wuint8 in v : nat.
+  Fail Check let v := 0%wuint8 in v : wuint.
   Compute wrap (Nat.to_uint 0).
 
   Notation wrap'' := wrap.
   Notation unwrap'' := unwrap.
-  Fail Numeral Notation wuint wrap'' unwrap'' : wuint_scope.
+  Fail Numeral Notation wuint wrap'' unwrap'' : wuint8'_scope.
+  Fail Check let v := 0%wuint8' in v : wuint.
 End Test8.
 
 Module Test9.
+  Delimit Scope wuint9_scope with wuint9.
+  Delimit Scope wuint9'_scope with wuint9'.
   Section with_let.
     Local Set Primitive Projections.
-    Record > wuint := wrap { unwrap : Decimal.uint }.
+    Record wuint := wrap { unwrap : Decimal.uint }.
     Let wrap' := wrap.
     Let unwrap' := unwrap.
     Local Notation wrap'' := wrap.
     Local Notation unwrap'' := unwrap.
-    Delimit Scope wuint_scope with wuint.
-    Fail Numeral Notation wuint wrap' unwrap' : wuint_scope.
-    Fail Numeral Notation wuint wrap'' unwrap'' : wuint_scope.
+    Numeral Notation wuint wrap' unwrap' : wuint9_scope.
+    Check let v := 0%wuint9 in v : wuint.
+    Fail Numeral Notation wuint wrap'' unwrap'' : wuint9'_scope.
+    Fail Check let v := 0%wuint9' in v : wuint.
   End with_let.
+  Check let v := 0%wuint9 in v : nat.
+  Fail Check let v := 0%wuint9 in v : wuint.
 End Test9.
 
 Module Test10.
@@ -175,3 +185,17 @@ Module Test10.
   (* Check that there is no warning here *)
   Numeral Notation unit of_any_uint to_uint : unit2_scope (abstract after 1).
 End Test10.
+
+Module Test11.
+  (* Test that numeral notations don't work on proof-local variables, especially not ones containing evars *)
+  Inductive unit11 := tt11.
+  Delimit Scope unit11_scope with unit11.
+  Goal True.
+    evar (to_uint : unit11 -> Decimal.uint).
+    evar (of_uint : Decimal.uint -> unit11).
+    Fail Numeral Notation unit11 of_uint to_uint : uint11_scope.
+    exact I.
+    Unshelve.
+    all: solve [ constructor ].
+  Qed.
+End Test11.
-- 
cgit v1.2.3


From 548976ac825298f27e6be00bbbb1be0752568f6f Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Thu, 16 Aug 2018 10:35:11 -0400
Subject: [numeral notations] support aliases

Aliases of global references can now be used in numeral notations
---
 test-suite/success/NumeralNotations.v | 37 +++++++++++++++++++++++++++++++----
 1 file changed, 33 insertions(+), 4 deletions(-)

(limited to 'test-suite')

diff --git a/test-suite/success/NumeralNotations.v b/test-suite/success/NumeralNotations.v
index e63b9dc4c7..5a58a1b72d 100644
--- a/test-suite/success/NumeralNotations.v
+++ b/test-suite/success/NumeralNotations.v
@@ -148,8 +148,8 @@ Module Test8.
 
   Notation wrap'' := wrap.
   Notation unwrap'' := unwrap.
-  Fail Numeral Notation wuint wrap'' unwrap'' : wuint8'_scope.
-  Fail Check let v := 0%wuint8' in v : wuint.
+  Numeral Notation wuint wrap'' unwrap'' : wuint8'_scope.
+  Check let v := 0%wuint8' in v : wuint.
 End Test8.
 
 Module Test9.
@@ -164,8 +164,8 @@ Module Test9.
     Local Notation unwrap'' := unwrap.
     Numeral Notation wuint wrap' unwrap' : wuint9_scope.
     Check let v := 0%wuint9 in v : wuint.
-    Fail Numeral Notation wuint wrap'' unwrap'' : wuint9'_scope.
-    Fail Check let v := 0%wuint9' in v : wuint.
+    Numeral Notation wuint wrap'' unwrap'' : wuint9'_scope.
+    Check let v := 0%wuint9' in v : wuint.
   End with_let.
   Check let v := 0%wuint9 in v : nat.
   Fail Check let v := 0%wuint9 in v : wuint.
@@ -199,3 +199,32 @@ Module Test11.
     all: solve [ constructor ].
   Qed.
 End Test11.
+
+Module Test12.
+  (* Test for numeral notations on context variables *)
+  Delimit Scope test12_scope with test12.
+  Section test12.
+    Context (to_uint : unit -> Decimal.uint) (of_uint : Decimal.uint -> unit).
+
+    Numeral Notation unit of_uint to_uint : test12_scope.
+    Check let v := 1%test12 in v : unit.
+  End test12.
+End Test12.
+
+Module Test13.
+  (* Test for numeral notations on notations which do not denote references *)
+  Delimit Scope test13_scope with test13.
+  Delimit Scope test13'_scope with test13'.
+  Delimit Scope test13''_scope with test13''.
+  Definition to_uint (x y : unit) : Decimal.uint := Nat.to_uint O.
+  Definition of_uint (x : Decimal.uint) : unit := tt.
+  Definition to_uint_good := to_uint tt.
+  Notation to_uint' := (to_uint tt).
+  Notation to_uint'' := (to_uint _).
+  Numeral Notation unit of_uint to_uint_good : test13_scope.
+  Check let v := 0%test13 in v : unit.
+  Fail Numeral Notation unit of_uint to_uint' : test13'_scope.
+  Fail Check let v := 0%test13' in v : unit.
+  Fail Numeral Notation unit of_uint to_uint'' : test13''_scope.
+  Fail Check let v := 0%test13'' in v : unit.
+End Test13.
-- 
cgit v1.2.3


From 6dcbbeb95682bbf470e58e25e0a357a84c3283b6 Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Thu, 23 Aug 2018 11:03:29 -0400
Subject: 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.
---
 test-suite/success/Compat88.v         | 18 ++++++++++++++++++
 test-suite/success/NumeralNotations.v | 19 +++++++++++++++++++
 2 files changed, 37 insertions(+)
 create mode 100644 test-suite/success/Compat88.v

(limited to 'test-suite')

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.
-- 
cgit v1.2.3


From e9d44aefa9d6058c72845788745468aa010708b5 Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Thu, 23 Aug 2018 15:10:58 -0400
Subject: Make Numeral Notation obey Local/Global

Thanks to Emilio and Pierre-Marie Pédrot for pointers.
---
 test-suite/success/NumeralNotations.v | 22 ++++++++++++++++++----
 1 file changed, 18 insertions(+), 4 deletions(-)

(limited to 'test-suite')

diff --git a/test-suite/success/NumeralNotations.v b/test-suite/success/NumeralNotations.v
index bacc982ccc..4521ad0e37 100644
--- a/test-suite/success/NumeralNotations.v
+++ b/test-suite/success/NumeralNotations.v
@@ -139,7 +139,7 @@ Module Test8.
     Context (dummy : unit).
     Definition wrap' := let __ := dummy in wrap.
     Definition unwrap' := let __ := dummy in unwrap.
-    Global Numeral Notation wuint wrap' unwrap' : wuint8_scope.
+    Numeral Notation wuint wrap' unwrap' : wuint8_scope.
     Check let v := 0%wuint8 in v : wuint.
   End with_var.
   Check let v := 0%wuint8 in v : nat.
@@ -231,19 +231,33 @@ 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. *)
+     also test that [Local Numeral Notation]s do not escape modules
+     nor sections. *)
   Delimit Scope test14_scope with test14.
   Delimit Scope test14'_scope with test14'.
+  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.
+    Check let v := 0%test14 in v : unit.
+    Check let v := 0%test14' in v : unit.
   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!! *)
+  Fail Check let v := 0%test14 in v : unit.
   Check let v := 0%test14' in v : unit.
+  Section InnerSection.
+    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.
+    Fail Global Numeral Notation unit of_uint to_uint : test14'''_scope.
+    Check let v := 0%test14'' in v : unit.
+    Fail Check let v := 0%test14''' in v : unit.
+  End InnerSection.
+  Fail Check let v := 0%test14'' in v : unit.
+  Fail Check let v := 0%test14''' in v : unit.
 End Test14.
-- 
cgit v1.2.3


From 31d58c9ee979699e733a561ec4eef6b0829fe73a Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Fri, 31 Aug 2018 15:22:26 -0400
Subject: Add some module tests to numeral notations

---
 test-suite/success/NumeralNotations.v | 41 +++++++++++++++++++++++++++++++++++
 1 file changed, 41 insertions(+)

(limited to 'test-suite')

diff --git a/test-suite/success/NumeralNotations.v b/test-suite/success/NumeralNotations.v
index 4521ad0e37..4a275de5b5 100644
--- a/test-suite/success/NumeralNotations.v
+++ b/test-suite/success/NumeralNotations.v
@@ -261,3 +261,44 @@ Module Test14.
   Fail Check let v := 0%test14'' in v : unit.
   Fail Check let v := 0%test14''' in v : unit.
 End Test14.
+
+Module Test15.
+  (** Test module include *)
+  Delimit Scope test15_scope with test15.
+  Module Inner.
+    Definition to_uint (x : unit) : Decimal.uint := Nat.to_uint O.
+    Definition of_uint (x : Decimal.uint) : unit := tt.
+    Numeral Notation unit of_uint to_uint : test15_scope.
+    Check let v := 0%test15 in v : unit.
+  End Inner.
+  Module Inner2.
+    Include Inner.
+    Check let v := 0%test15 in v : unit.
+  End Inner2.
+  Import Inner Inner2.
+  Check let v := 0%test15 in v : unit.
+End Test15.
+
+Module Test16.
+  (** Test functors *)
+  Delimit Scope test16_scope with test16.
+  Module Type A.
+    Axiom T : Set.
+    Axiom t : T.
+  End A.
+  Module F (a : A).
+    Inductive Foo := foo (_ : a.T).
+    Definition to_uint (x : Foo) : Decimal.uint := Nat.to_uint O.
+    Definition of_uint (x : Decimal.uint) : Foo := foo a.t.
+    Numeral Notation Foo of_uint to_uint : test16_scope.
+    Check let v := 0%test16 in v : Foo. (* Prints wrong: let v := foo a.t in v : Foo *)
+  End F.
+  Module a <: A.
+    Definition T : Set := unit.
+    Definition t : T := tt.
+  End a.
+  Module Import f := F a.
+  (* Check let v := 0%test16 in v : Foo. *)
+  (* Error: Anomaly "Uncaught exception Failure("List.last")."
+Please report at http://coq.inria.fr/bugs/. *)
+End Test16.
-- 
cgit v1.2.3


From 17cb475550a0f4efe9f3f4c58fdbd9039f5fdd68 Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Fri, 31 Aug 2018 17:01:43 -0400
Subject: Give a proper error message on num-not in functor

Numeral Notations are not well-supported inside functors.  We now give a
proper error message rather than an anomaly when this occurs.
---
 test-suite/success/NumeralNotations.v | 10 ++++------
 1 file changed, 4 insertions(+), 6 deletions(-)

(limited to 'test-suite')

diff --git a/test-suite/success/NumeralNotations.v b/test-suite/success/NumeralNotations.v
index 4a275de5b5..47ef381270 100644
--- a/test-suite/success/NumeralNotations.v
+++ b/test-suite/success/NumeralNotations.v
@@ -1,4 +1,3 @@
-
 (* Test that we fail, rather than raising anomalies, on opaque terms during interpretation *)
 
 (* https://github.com/coq/coq/pull/8064#discussion_r202497516 *)
@@ -290,15 +289,14 @@ Module Test16.
     Inductive Foo := foo (_ : a.T).
     Definition to_uint (x : Foo) : Decimal.uint := Nat.to_uint O.
     Definition of_uint (x : Decimal.uint) : Foo := foo a.t.
-    Numeral Notation Foo of_uint to_uint : test16_scope.
-    Check let v := 0%test16 in v : Foo. (* Prints wrong: let v := foo a.t in v : Foo *)
+    Global Numeral Notation Foo of_uint to_uint : test16_scope.
+    Check let v := 0%test16 in v : Foo.
   End F.
   Module a <: A.
     Definition T : Set := unit.
     Definition t : T := tt.
   End a.
   Module Import f := F a.
-  (* Check let v := 0%test16 in v : Foo. *)
-  (* Error: Anomaly "Uncaught exception Failure("List.last")."
-Please report at http://coq.inria.fr/bugs/. *)
+  (** Ideally this should work, but it should definitely not anomaly *)
+  Fail Check let v := 0%test16 in v : Foo.
 End Test16.
-- 
cgit v1.2.3