20 files changed, 361 insertions, 13 deletions
diff --git a/test-suite/bugs/closed/bug_13249.v b/test-suite/bugs/closed/bug_13249.v
new file mode 100644
index 0000000000..06f7ddbd3a
--- /dev/null
+++ b/test-suite/bugs/closed/bug_13249.v
@@ -0,0 +1,9 @@
+Global Generalizable All Variables.
+
+Section test.
+  Context {A : Type}.
+  Context `{!foo A}.
+
+  Goal foo A.
+  Proof. assumption. Defined.
+End test.
diff --git a/test-suite/bugs/closed/bug_13300.v b/test-suite/bugs/closed/bug_13300.v
new file mode 100644
index 0000000000..e4fcd6dacc
--- /dev/null
+++ b/test-suite/bugs/closed/bug_13300.v
@@ -0,0 +1,7 @@
+Polymorphic Definition type := Type.
+
+Inductive bad : type := .
+
+Fail Check bad : Prop.
+Check bad : Set.
+(* lowered as much as possible *)
diff --git a/test-suite/bugs/closed/bug_13366.v b/test-suite/bugs/closed/bug_13366.v
new file mode 100644
index 0000000000..06918a9266
--- /dev/null
+++ b/test-suite/bugs/closed/bug_13366.v
@@ -0,0 +1,5 @@
+Class Functor (F : Type -> Type) : Type :=
+  fmap : F nat.
+
+Fail Definition blah := sum fmap.
+(* used to be anomaly not an arity *)
diff --git a/test-suite/bugs/closed/bug_9809.v b/test-suite/bugs/closed/bug_9809.v
new file mode 100644
index 0000000000..4a7d2c7fac
--- /dev/null
+++ b/test-suite/bugs/closed/bug_9809.v
@@ -0,0 +1,30 @@
+Section FreeMonad.
+
+  Variable S : Type.
+  Variable P : S -> Type.
+
+  Inductive FreeF A : Type :=
+  | retFree : A -> FreeF A
+  | opr     : forall s, (P s -> FreeF A) -> FreeF A.
+
+End FreeMonad.
+
+Section Fibonnacci.
+
+  Inductive gen_op := call_op : nat -> gen_op.
+  Definition gen_ty (op : gen_op) :=
+    match op with
+    | call_op _ => nat
+    end.
+
+  Fail Definition fib0 (n:nat) : FreeF gen_op gen_ty nat :=
+    match n  with
+    | 0
+    | 1 => retFree _ _ _ 1
+    | S (S k) =>
+      opr _ _ _ (call_op (S k))
+          (fun r1 => opr _ _ _ (call_op k)
+                      (fun r0 => retFree (* _ _ _ *) (r1 + r0)))
+    end.
+
+End Fibonnacci.
diff --git a/test-suite/bugs/closed/bug_9971.v b/test-suite/bugs/closed/bug_9971.v
new file mode 100644
index 0000000000..ef526dcd7d
--- /dev/null
+++ b/test-suite/bugs/closed/bug_9971.v
@@ -0,0 +1,27 @@
+(* Test that it raises a normal error and not an anomaly *)
+Set Primitive Projections.
+Record prod A B := pair { fst : A ; snd : B }.
+Arguments fst {A B} _.
+Arguments snd {A B} _.
+Arguments pair {A B} _ _.
+Record piis := { dep_types : Type; indep_args : dep_types -> Type }.
+Import EqNotations.
+Goal forall (id : Set) (V : id) (piiio : id -> piis)
+            (Z : {ridc : id & prod (dep_types (piiio ridc)) True})
+            (P : dep_types (piiio V) -> Type) (W : {x : dep_types (piiio V) & P x}),
+    let ida := fun (x : id) (y : dep_types (piiio x)) => indep_args (piiio x) y in
+    prod True (ida V (projT1 W)) ->
+    Z = existT _ V (pair (projT1 W) I) ->
+    ida (projT1 Z) (fst (projT2 Z)).
+  intros.
+  refine  (rew <- [fun k' => ida (projT1 k') (fst (projT2 k'))]
+               H in
+              let v := I in
+              _);
+    refine (snd X).
+  Undo.
+Fail refine (rew <- [fun k' => ida (projT1 k') (fst (projT2 k'))]
+              H in
+             let v := I in
+             snd X).
+Abort.
diff --git a/test-suite/output/Notations3.out b/test-suite/output/Notations3.out
index 623ca316c9..a9bed49922 100644
--- a/test-suite/output/Notations3.out
+++ b/test-suite/output/Notations3.out
@@ -120,14 +120,14 @@ where
 letpair x [1] = {0};
 return (1, 2, 3, 4)
      : nat * nat * nat * nat
-{{ 1 | 1 // 1 }}
-     : nat
-!!! _ _ : nat, True
-     : (nat -> Prop) * ((nat -> Prop) * Prop)
 ((*1).2).3
      : nat
 *(1.2)
      : nat
+{{ 1 | 1 // 1 }}
+     : nat
+!!! _ _ : nat, True
+     : (nat -> Prop) * ((nat -> Prop) * Prop)
 ! '{{x, y}}, x.y = 0
      : Prop
 exists x : nat,
diff --git a/test-suite/output/Notations3.v b/test-suite/output/Notations3.v
index ce97d909a7..04a91c14d9 100644
--- a/test-suite/output/Notations3.v
+++ b/test-suite/output/Notations3.v
@@ -181,6 +181,13 @@ Notation "'letpair' x [1] = { a } ; 'return' ( b0 , b1 , .. , b2 )" :=
   (let x:=a in ( .. (b0,b1) .., b2)).
 Check letpair x [1] = {0}; return (1,2,3,4).
 
+(* Allow level for leftmost nonterminal when printing-only, BZ#5739 *)
+
+Notation "* x" := (id x) (only printing, at level 15, format "* x").
+Notation "x . y" := (x + y) (only printing, at level 20, x at level 14, left associativity, format "x . y").
+Check (((id 1) + 2) + 3).
+Check (id (1 + 2)).
+
 (* Test spacing in #5569 *)
 
 Notation "{ { xL | xR // xcut } }" := (xL+xR+xcut)
@@ -191,13 +198,6 @@ Check 1+1+1.
 Notation "!!! x .. y , b" := ((fun x => b), .. ((fun y => b), True) ..) (at level 200, x binder).
 Check !!! (x y:nat), True.
 
-(* Allow level for leftmost nonterminal when printing-only, BZ#5739 *)
-
-Notation "* x" := (id x) (only printing, at level 15, format "* x").
-Notation "x . y" := (x + y) (only printing, at level 20, x at level 14, left associativity, format "x . y").
-Check (((id 1) + 2) + 3).
-Check (id (1 + 2)).
-
 (* Test contraction of "forall x, let 'pat := x in ..." into "forall 'pat, ..." *)
 (* for isolated "forall" (was not working already in 8.6) *)
 Notation "! x .. y , A" := (id (forall x, .. (id (forall y, A)) .. )) (at level 200, x binder).
diff --git a/test-suite/output/Notations4.out b/test-suite/output/Notations4.out
index a6fd39c29b..86c4b3cccc 100644
--- a/test-suite/output/Notations4.out
+++ b/test-suite/output/Notations4.out
@@ -179,3 +179,21 @@ Found an inductive type while a pattern was expected.
      : Prop
 !!!! (nat, id), nat = true /\ id = false
      : Prop
+∀ x : nat, x = 0
+     : Prop
+∀₁ x, x = 0
+     : Prop
+∀₁ x, x = 0
+     : Prop
+∀₂ x y, x + y = 0
+     : Prop
+((1, 2))
+     : nat * nat
+%% [x == 1]
+     : Prop
+%%% [1]
+     : Prop
+[[2]]
+     : nat * nat
+%%%
+     : Type
diff --git a/test-suite/output/Notations4.v b/test-suite/output/Notations4.v
index 0731819bba..6af192ea82 100644
--- a/test-suite/output/Notations4.v
+++ b/test-suite/output/Notations4.v
@@ -414,3 +414,76 @@ Module P.
   End NotationBinderNotMixedWithTerms.
 
 End P.
+
+Module MorePrecise1.
+
+(* A notation with limited iteration is strictly more precise than a
+   notation with unlimited iteration *)
+
+Notation "∀ x .. y , P" := (forall x, .. (forall y, P) ..)
+  (at level 200, x binder, y binder, right associativity,
+  format "'[  ' '[  ' ∀  x  ..  y ']' ,  '/' P ']'") : type_scope.
+
+Check forall x, x = 0.
+
+Notation "∀₁ z , P" := (forall z, P)
+  (at level 200, right associativity) : type_scope.
+
+Check forall x, x = 0.
+
+Notation "∀₂ y x , P" := (forall y x, P)
+  (at level 200, right associativity) : type_scope.
+
+Check forall x, x = 0.
+Check forall x y, x + y = 0.
+
+Notation "(( x , y ))" := (x,y) : core_scope.
+
+Check ((1,2)).
+
+End MorePrecise1.
+
+Module MorePrecise2.
+
+(* Case of a bound binder *)
+Notation "%% [ x == y ]" := (forall x, S x = y) (at level 0, x pattern, y at level 60).
+
+(* Case of an internal binder *)
+Notation "%%% [ y ]" := (forall x : nat, x = y) (at level 0).
+
+(* Check that the two previous notations are indeed finer *)
+Notation "∀ x .. y , P" := (forall x, .. (forall y, P) ..)
+  (at level 200, x binder, y binder, right associativity,
+  format "'[  ' '[  ' ∀  x  ..  y ']' ,  '/' P ']'").
+Notation "∀' x .. y , P" := (forall y, .. (forall x, P) ..)
+  (at level 200, x binder, y binder, right associativity,
+  format "'[  ' '[  ' ∀'  x  ..  y ']' ,  '/' P ']'").
+
+Check %% [x == 1].
+Check %%% [1].
+
+Notation "[[ x ]]" := (pair 1 x).
+
+Notation "( x ; y ; .. ; z )" := (pair .. (pair x y) .. z).
+Notation "[ x ; y ; .. ; z ]" := (pair .. (pair x z) .. y).
+
+(* Check which is finer *)
+Check [[ 2 ]].
+
+End MorePrecise2.
+
+Module MorePrecise3.
+
+(* This is about a binder not bound in a notation being strictly more
+   precise than a binder bound in the notation (since the notation
+   applies - a priori - stricly less often) *)
+
+Notation "%%%" := (forall x, x) (at level 0).
+
+Notation "∀ x .. y , P" := (forall x, .. (forall y, P) ..)
+  (at level 200, x binder, y binder, right associativity,
+  format "'[  ' '[  ' ∀  x  ..  y ']' ,  '/' P ']'").
+
+Check %%%.
+
+End MorePrecise3.
diff --git a/test-suite/output/attributes.out b/test-suite/output/attributes.out
new file mode 100644
index 0000000000..25572ee2aa
--- /dev/null
+++ b/test-suite/output/attributes.out
@@ -0,0 +1,11 @@
+The command has indeed failed with message:
+Attribute for canonical specified twice.
+The command has indeed failed with message:
+key 'polymorphic' has been already set.
+The command has indeed failed with message:
+Invalid value 'foo' for key polymorphic
+use one of {yes, no}
+The command has indeed failed with message:
+Invalid syntax polymorphic(foo), try polymorphic={yes, no} instead.
+The command has indeed failed with message:
+Invalid syntax polymorphic(foo, bar), try polymorphic={yes, no} instead.
diff --git a/test-suite/output/attributes.v b/test-suite/output/attributes.v
new file mode 100644
index 0000000000..aef05e6cd4
--- /dev/null
+++ b/test-suite/output/attributes.v
@@ -0,0 +1,9 @@
+Fail #[canonical=yes, canonical=no] Definition a := 3.
+
+Fail #[universes(polymorphic=yes,polymorphic=no)] Definition a := 3.
+
+Fail #[universes(polymorphic=foo)] Definition a := 3.
+
+Fail #[universes(polymorphic(foo))] Definition a := 3.
+
+Fail #[universes(polymorphic(foo,bar))] Definition a := 3.
diff --git a/test-suite/output/bug_10824.out b/test-suite/output/bug_10824.out
new file mode 100644
index 0000000000..4bc5aafbca
--- /dev/null
+++ b/test-suite/output/bug_10824.out
@@ -0,0 +1,4 @@
+!!
+     : Prop
+!!
+     : Prop
diff --git a/test-suite/output/bug_10824.v b/test-suite/output/bug_10824.v
new file mode 100644
index 0000000000..01271f7d61
--- /dev/null
+++ b/test-suite/output/bug_10824.v
@@ -0,0 +1,12 @@
+Module A.
+Notation F := False.
+Notation "!!" := False (at level 100).
+Check False.
+End A.
+
+Module B.
+Notation "!!" := False (at level 100).
+Notation F := False.
+Notation "!!" := False (at level 100).
+Check False.
+End B.
diff --git a/test-suite/output/bug_7443.out b/test-suite/output/bug_7443.out
new file mode 100644
index 0000000000..446ec6a1ad
--- /dev/null
+++ b/test-suite/output/bug_7443.out
@@ -0,0 +1,13 @@
+Literal 1
+     : Type
+[1]
+     : Type
+Literal 1
+     : Type
+[1]
+     : Type
+The command has indeed failed with message:
+The term "1" has type "Datatypes.nat" while it is expected to have type
+ "denote ?t".
+Literal 1
+     : Type
diff --git a/test-suite/output/bug_7443.v b/test-suite/output/bug_7443.v
new file mode 100644
index 0000000000..33f76dbcfa
--- /dev/null
+++ b/test-suite/output/bug_7443.v
@@ -0,0 +1,37 @@
+Inductive type := nat | bool.
+Definition denote (t : type)
+  := match t with
+     | nat => Datatypes.nat
+     | bool => Datatypes.bool
+     end.
+Ltac reify t :=
+  lazymatch eval cbv beta in t with
+  | Datatypes.nat => nat
+  | Datatypes.bool => bool
+  end.
+Notation reify t := (ltac:(let rt := reify t in exact rt)) (only parsing).
+Notation reify_type_of e := (reify ((fun t (_ : t) => t) _ e)) (only parsing).
+Axiom Literal : forall {t}, denote t -> Type.
+Declare Scope foo_scope.
+Delimit Scope foo_scope with foo.
+Open Scope foo_scope.
+Section A.
+  Notation "[ x ]" := (Literal (t:=reify_type_of x) x) (only parsing) : foo_scope.
+  Check [1]. (* Literal 1 : Type *) (* as expected *)
+  Notation "[ x ]" := (Literal x) : foo_scope.
+  Check @Literal nat 1. (* Incorred: gives Literal 1 : Type when it should give [1]. Fixed by #12950 *)
+  Notation "[ x ]" := (Literal (t:=reify_type_of x) x) (only parsing) : foo_scope.
+  Check [1]. (* Incorrect: gives Literal 1 : Type when it should give [1]. This is disputable:
+  #12950 considers that giving an only parsing a previous both-parsing-and-printing notation *)
+End A.
+Section B.
+  Notation "[ x ]" := (Literal x) : foo_scope.
+  Check @Literal nat 1. (* [1] : Type *)
+  Fail Check [1]. (* As expected: The command has indeed failed with message:
+  The term "1" has type "Datatypes.nat" while it is expected to have type
+   "denote ?t". *)
+  Notation "[ x ]" := (Literal (t:=reify_type_of x) x) (only parsing) : foo_scope.
+  Check [1]. (* Should succeed, but instead fails with: Error:
+  The term "1" has type "Datatypes.nat" while it is expected to have type
+  "denote ?t". Fixed by #12950, but previous declaration is cancelled by #12950. *)
+End B.
diff --git a/test-suite/output/bug_9569.out b/test-suite/output/bug_9569.out
new file mode 100644
index 0000000000..2d474e4933
--- /dev/null
+++ b/test-suite/output/bug_9569.out
@@ -0,0 +1,16 @@
+1 subgoal
+  
+  ============================
+  exists I : True, I = Logic.I
+1 subgoal
+  
+  ============================
+  f True False True False (Logic.True /\ Logic.False)
+1 subgoal
+  
+  ============================
+  [I | I = Logic.I; I = Logic.I] = [I | I = Logic.I; I = Logic.I]
+1 subgoal
+  
+  ============================
+  [I & I = Logic.I | I = Logic.I; Logic.I = I]
diff --git a/test-suite/output/bug_9569.v b/test-suite/output/bug_9569.v
new file mode 100644
index 0000000000..ee5b052811
--- /dev/null
+++ b/test-suite/output/bug_9569.v
@@ -0,0 +1,18 @@
+Goal exists I, I = Logic.I.
+Show.
+Abort.
+
+Notation f x y p q r := ((forall x, p /\ r) /\ forall y, q /\ r).
+Goal f True False True False (Logic.True /\ Logic.False).
+Show.
+Abort.
+
+Notation "[ x | y ; z ; .. ; t ]" := (pair .. (pair (forall x, y) (forall x, z)) .. (forall x, t)).
+Goal [ I | I = Logic.I ; I = Logic.I ] = [ I | I = Logic.I ; I = Logic.I ].
+Show.
+Abort.
+
+Notation "[ x & p | y ; .. ; z ; t ]" := (forall x, p -> y -> .. (forall x, p -> z -> forall x, p -> t) ..).
+Goal [ I & I = Logic.I | I = Logic.I ; Logic.I = I ].
+Show.
+Abort.
diff --git a/test-suite/primitive/float/next_up_down.v b/test-suite/primitive/float/next_up_down.v
index 4f8427dc5b..ea45fb3983 100644
--- a/test-suite/primitive/float/next_up_down.v
+++ b/test-suite/primitive/float/next_up_down.v
@@ -120,3 +120,46 @@ Check (eq_refl (SF64succ (Prim2SF f14)) <<: Prim2SF (next_up f14) = SF64succ (Pr
 Check (eq_refl (SF64pred (Prim2SF f14)) <<: Prim2SF (next_down f14) = SF64pred (Prim2SF f14)).
 Check (eq_refl (SF64succ (Prim2SF f15)) <<: Prim2SF (next_up f15) = SF64succ (Prim2SF f15)).
 Check (eq_refl (SF64pred (Prim2SF f15)) <<: Prim2SF (next_down f15) = SF64pred (Prim2SF f15)).
+
+Check (eq_refl : next_up nan = nan).
+Check (eq_refl : next_down nan = nan).
+Check (eq_refl : next_up neg_infinity = -0x1.fffffffffffffp+1023).
+Check (eq_refl : next_down neg_infinity = neg_infinity).
+Check (eq_refl : next_up (-0x1.fffffffffffffp+1023) = -0x1.ffffffffffffep+1023).
+Check (eq_refl : next_down (-0x1.fffffffffffffp+1023) = neg_infinity).
+Check (eq_refl : next_up (-0x1.ffffffffffffap+1023) = -0x1.ffffffffffff9p+1023).
+Check (eq_refl : next_down (-0x1.ffffffffffffap+1023) = -0x1.ffffffffffffbp+1023).
+Check (eq_refl : next_up (-0x1.fffffffffffff) = -0x1.ffffffffffffe).
+Check (eq_refl : next_down (-0x1.fffffffffffff) = -0x1p+1).
+Check (eq_refl : next_up (-0x1p1) = -0x1.fffffffffffff).
+Check (eq_refl : next_down (-0x1p1) = -0x1.0000000000001p+1).
+Check (eq_refl : next_up (-0x1p-1022) = -0x0.fffffffffffffp-1022).
+Check (eq_refl : next_down (-0x1p-1022) = -0x1.0000000000001p-1022).
+Check (eq_refl : next_up (-0x0.fffffffffffffp-1022) = -0x0.ffffffffffffep-1022).
+Check (eq_refl : next_down (-0x0.fffffffffffffp-1022) = -0x1p-1022).
+Check (eq_refl : next_up (-0x0.01p-1022) = -0x0.00fffffffffffp-1022).
+Check (eq_refl : next_down (-0x0.01p-1022) = -0x0.0100000000001p-1022).
+Check (eq_refl : next_up (-0x0.0000000000001p-1022) = -0).
+Check (eq_refl : next_down (-0x0.0000000000001p-1022) = -0x0.0000000000002p-1022).
+Check (eq_refl : next_up (-0) = 0x0.0000000000001p-1022).
+Check (eq_refl : next_down (-0) = -0x0.0000000000001p-1022).
+Check (eq_refl : next_up 0 = 0x0.0000000000001p-1022).
+Check (eq_refl : next_down 0 = -0x0.0000000000001p-1022).
+Check (eq_refl : next_up 0x0.0000000000001p-1022 = 0x0.0000000000002p-1022).
+Check (eq_refl : next_down 0x0.0000000000001p-1022 = 0).
+Check (eq_refl : next_up 0x0.01p-1022 = 0x0.0100000000001p-1022).
+Check (eq_refl : next_down 0x0.01p-1022 = 0x0.00fffffffffffp-1022).
+Check (eq_refl : next_up 0x0.fffffffffffffp-1022 = 0x1p-1022).
+Check (eq_refl : next_down 0x0.fffffffffffffp-1022 = 0x0.ffffffffffffep-1022).
+Check (eq_refl : next_up 0x1p-1022 = 0x1.0000000000001p-1022).
+Check (eq_refl : next_down 0x1p-1022 = 0x0.fffffffffffffp-1022).
+Check (eq_refl : next_up 0x1p1 = 0x1.0000000000001p+1).
+Check (eq_refl : next_down 0x1p1 = 0x1.fffffffffffff).
+Check (eq_refl : next_up 0x1.fffffffffffff = 0x1p+1).
+Check (eq_refl : next_down 0x1.fffffffffffff = 0x1.ffffffffffffe).
+Check (eq_refl : next_up 0x1.ffffffffffffap+1023 = 0x1.ffffffffffffbp+1023).
+Check (eq_refl : next_down 0x1.ffffffffffffap+1023 = 0x1.ffffffffffff9p+1023).
+Check (eq_refl : next_up 0x1.fffffffffffffp+1023 = infinity).
+Check (eq_refl : next_down 0x1.fffffffffffffp+1023 = 0x1.ffffffffffffep+1023).
+Check (eq_refl : next_up infinity = infinity).
+Check (eq_refl : next_down infinity = 0x1.fffffffffffffp+1023).
diff --git a/test-suite/success/Template.v b/test-suite/success/Template.v
index 656362b8fc..d11ae20b8d 100644
--- a/test-suite/success/Template.v
+++ b/test-suite/success/Template.v
@@ -37,7 +37,7 @@ Module Yes.
 End Yes.
 
 Module No.
-  #[universes(notemplate)]
+  #[universes(template=no)]
   Inductive Box (A:Type) : Type := box : A -> Box A.
 
   About Box.
diff --git a/test-suite/success/attribute_syntax.v b/test-suite/success/attribute_syntax.v
index b403fc120c..b866c4b074 100644
--- a/test-suite/success/attribute_syntax.v
+++ b/test-suite/success/attribute_syntax.v
@@ -16,11 +16,16 @@ Definition ι T (x: T) := x.
 
 Check ι _ ι.
 
+#[universes(polymorphic=no)]
+Definition ιι T (x: T) := x.
+
+Fail Check ιι _ ιι.
+
 #[program]
 Fixpoint f (n: nat) {wf lt n} : nat := _.
 Reset f.
 
-#[program(true)]
+#[program=yes]
 Fixpoint f (n: nat) {wf lt n} : nat := _.
 Reset f.
 
@@ -43,3 +48,14 @@ Export Set Foo.
 
 Fail #[ export ] Export Foo.
 (* Attribute for Locality specified twice *)
+
+(* Tests for deprecated attribute syntax *)
+Set Warnings "-deprecated-attribute-syntax".
+
+#[program(true)]
+Fixpoint f (n: nat) {wf lt n} : nat := _.
+Reset f.
+
+#[universes(monomorphic)]
+Definition ιιι T (x: T) := x.
+Fail Check ιιι _ ιιι.