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

2 files changed, 167 insertions, 14 deletions

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.