9 files changed, 154 insertions, 4 deletions
diff --git a/test-suite/Makefile b/test-suite/Makefile
index 2a2f62e23f..f06439a863 100644
--- a/test-suite/Makefile
+++ b/test-suite/Makefile
@@ -517,6 +517,17 @@ approve-output: output output-coqtop output-coqchk
 	  echo "Updated $${f%.real}!"; \
 	done
 
+approve-coqdoc: coqdoc
+	$(HIDE)(cd coqdoc; \
+	for f in *.html.out; do \
+	  cp "Coqdoc.$${f%.out}" "$$f"; \
+	  echo "Updated $$f!"; \
+	done; \
+	for f in *.tex.out; do \
+	  cat "Coqdoc.$${f%.out}" | grep -v "^%%" > "$$f"; \
+	  echo "Updated $$f!"; \
+	done)
+
 # the expected output for the MExtraction test is
 # /plugins/micromega/micromega.ml except with additional newline
 output/MExtraction.out: ../plugins/micromega/micromega.ml
diff --git a/test-suite/bugs/closed/bug_11866.v b/test-suite/bugs/closed/bug_11866.v
new file mode 100644
index 0000000000..5a47f3833e
--- /dev/null
+++ b/test-suite/bugs/closed/bug_11866.v
@@ -0,0 +1,43 @@
+Require Import Ltac2.Ltac2.
+
+Ltac2 Notation "ex0" x(tactic(0)) := ().
+Ltac2 Notation "ex1" x(tactic(1)) := ().
+Ltac2 Notation "ex2" x(tactic(2)) := ().
+Ltac2 Notation "ex3" x(tactic(3)) := ().
+Ltac2 Notation "ex4" x(tactic(4)) := ().
+Ltac2 Notation "ex5" x(tactic(5)) := ().
+Ltac2 Notation "ex6" x(tactic(6)) := ().
+
+Ltac2 Notation ":::0" x(tactic) "+0" y(tactic) : 0 := ().
+Ltac2 Notation ":::1" x(tactic) "+1" y(tactic) : 1 := ().
+Ltac2 Notation ":::2" x(tactic) "+2" y(tactic) : 2 := ().
+Ltac2 Notation ":::3" x(tactic) "+3" y(tactic) : 3 := ().
+Ltac2 Notation ":::4" x(tactic) "+4" y(tactic) : 4 := ().
+Ltac2 Notation ":::5" x(tactic) "+5" y(tactic) : 5 := ().
+Ltac2 Notation ":::6" x(tactic) "+6" y(tactic) : 6 := ().
+Fail Ltac2 Notation ":::7" x(tactic) "+7" y(tactic) : 7 := ().
+Goal True.
+  ex0 :::0 0 +0 0.
+  ex1 :::0 0 +0 0.
+  (*ex2 :::0 0 +0 0.*) (* fails with an anomaly, cf COQBUG(https://github.com/coq/coq/issues/12807) *)
+  (*ex3 :::0 0 +0 0.*)
+  ex4 :::0 0 +0 0.
+  ex5 :::0 0 +0 0.
+  ex6 :::0 0 +0 0.
+
+  ex0 :::1 0 +1 0.
+  ex1 :::1 0 +1 0.
+  (*ex2 :::1 0 +1 0.*)
+  (*ex3 :::1 0 +1 0.*)
+  ex4 :::1 0 +1 0.
+  ex5 :::1 0 +1 0.
+  ex6 :::1 0 +1 0.
+
+  ex0 :::6 0 +6 0.
+  ex1 :::6 0 +6 0.
+  (*ex2 :::6 0 +6 0.*)
+  (*ex3 :::6 0 +6 0.*)
+  ex4 :::6 0 +6 0.
+  ex5 :::6 0 +6 0.
+  ex6 :::6 0 +6 0.
+Abort.
diff --git a/test-suite/bugs/closed/bug_14131.v b/test-suite/bugs/closed/bug_14131.v
new file mode 100644
index 0000000000..611464458e
--- /dev/null
+++ b/test-suite/bugs/closed/bug_14131.v
@@ -0,0 +1,19 @@
+Set Implicit Arguments.
+Unset Elimination Schemes.
+
+Inductive JMeq (A:Type) (x:A) : forall B:Type, B -> Prop :=
+    JMeq_refl : JMeq x x.
+
+Set Elimination Schemes.
+
+Register JMeq as core.JMeq.type.
+
+Axiom JMeq_ind : forall (A:Type) (x:A) (P:A -> Prop),
+  P x -> forall y, JMeq x y -> P y.
+
+Register JMeq_ind as core.JMeq.ind.
+
+Lemma JMeq_ind_r : forall (A:Type) (x:A) (P:A -> Prop),
+   P x -> forall y, JMeq y x -> P y.
+Proof. intros. try rewrite H0.
+Abort.
diff --git a/test-suite/bugs/closed/bug_3468.v b/test-suite/bugs/closed/bug_3468.v
index 6ff394bca6..8d7d97d7aa 100644
--- a/test-suite/bugs/closed/bug_3468.v
+++ b/test-suite/bugs/closed/bug_3468.v
@@ -26,4 +26,5 @@ Notation "& b" := ltac:(exact (b)%my) (at level 100, only parsing): my_scope.
 Definition test := (& (@4))%my.
 
 (* Check inconsistent scopes *)
+Set Warnings "+inconsistent-scopes".
 Fail Notation bar3 a := (let __ := ltac:(exact a%nat) in a%bool) (only parsing).
diff --git a/test-suite/output/Warnings.out b/test-suite/output/Warnings.out
index a70f8ca45a..23119bab97 100644
--- a/test-suite/output/Warnings.out
+++ b/test-suite/output/Warnings.out
@@ -1,3 +1,4 @@
 File "stdin", line 4, characters 0-22:
-Warning: Projection value has no head constant: fun x : B => x in canonical
-instance a of b, ignoring it. [projection-no-head-constant,typechecker]
+Warning: Projection value has no head constant: forall x : nat, x > 0 in
+canonical instance a of b, ignoring it.
+[projection-no-head-constant,typechecker]
diff --git a/test-suite/output/Warnings.v b/test-suite/output/Warnings.v
index 7465442cab..ce92bcbbb2 100644
--- a/test-suite/output/Warnings.v
+++ b/test-suite/output/Warnings.v
@@ -1,5 +1,5 @@
 (* Term in warning was not printed in the right environment at some time *)
-Record A := { B:Type; b:B->B }.
-Definition a B := {| B:=B; b:=fun x => x |}.
+Record A := { B:Type; b:Prop }.
+Definition a B := {| B:=B; b:=forall x, x > 0 |}.
 Canonical Structure a.
 
diff --git a/test-suite/output/notation_principal_scope.out b/test-suite/output/notation_principal_scope.out
new file mode 100644
index 0000000000..5ccee259b0
--- /dev/null
+++ b/test-suite/output/notation_principal_scope.out
@@ -0,0 +1,20 @@
+The command has indeed failed with message:
+Argument X was previously inferred to be in scope function_scope but is here
+used in the empty scope stack. Scope function_scope will be used at parsing
+time unless you override it by annotating the argument with an explicit scope
+of choice. [inconsistent-scopes,syntax]
+The command has indeed failed with message:
+Simple notations don't support only printing
+The command has indeed failed with message:
+The reference nonexisting was not found in the current environment.
+The command has indeed failed with message:
+Notation scope for argument X can be specified only once.
+pp I
+     : True /\ True
+The command has indeed failed with message:
+Illegal application (Non-functional construction): 
+The expression "I" of type "True" cannot be applied to the term
+ "I" : "True"
+File "stdin", line 21, characters 0-50:
+Warning: This notation will not be used for printing as it is bound to a
+single variable. [notation-bound-to-variable,parsing]
diff --git a/test-suite/output/notation_principal_scope.v b/test-suite/output/notation_principal_scope.v
new file mode 100644
index 0000000000..6bd911501d
--- /dev/null
+++ b/test-suite/output/notation_principal_scope.v
@@ -0,0 +1,23 @@
+Arguments conj {_ _} _ _%function.
+
+Set Warnings "+inconsistent-scopes".
+Fail Notation pp X := (conj X X).
+
+Fail Notation pp := 1 (only printing).
+
+Fail Notation pp X := nonexisting.
+
+Fail Notation pp X := (conj X X) (X, X in scope nat_scope).
+
+Notation pp X := (conj X X) (X in scope nat_scope).
+
+Notation "$" := I (only parsing) : nat_scope.
+Notation "$" := (I I) (only parsing) : bool_scope.
+
+Open Scope bool_scope.
+Check pp $.
+Fail Check pp (id $).
+
+Notation pp1 X := (X%nat) (X in scope bool_scope).
+Notation pp2 X := ((X + X)%type) (X in scope bool_scope).
+Notation pp3 X := (((X, X)%type, X)%nat) (X in scope bool_scope).
diff --git a/test-suite/success/CanonicalStructure.v b/test-suite/success/CanonicalStructure.v
index 88702a6e80..a833dd0bd6 100644
--- a/test-suite/success/CanonicalStructure.v
+++ b/test-suite/success/CanonicalStructure.v
@@ -70,3 +70,35 @@ Section W.
   Check (refl_equal _ : l _ = x2).
 End W.
 Fail Check (refl_equal _ : l _ = x2).
+
+(* Lambda keys *)
+Section L1.
+  Structure cs_lambda := { cs_lambda_key : nat -> nat }.
+  #[local] Canonical Structure cs_lambda_func :=
+    {| cs_lambda_key := fun x => x + 1 |}.
+  Check (refl_equal _ : cs_lambda_key _ = fun _ => _ + _).
+End L1.
+
+Section L2.
+  #[local] Canonical Structure cs_lambda_func2 :=
+    {| cs_lambda_key := fun x => 1 + x |}.
+  Check (refl_equal _ : cs_lambda_key _ = fun x => 1 + x).
+End L2.
+
+Section L3.
+  #[local] Canonical Structure cs_lambda_func3 :=
+    {| cs_lambda_key := fun x => 1 + x |}.
+  Check (refl_equal _ : cs_lambda_key _ = Nat.add 1).
+End L3.
+
+Section L4.
+  #[local] Canonical Structure cs_lambda_func4 :=
+    {| cs_lambda_key := Nat.add 1 |}.
+  Check (refl_equal _ : cs_lambda_key _ = Nat.add 1).
+End L4.
+
+Section L5.
+  #[local] Canonical Structure cs_lambda_func5 :=
+    {| cs_lambda_key := Nat.add 1 |}.
+  Check (refl_equal _ : cs_lambda_key _ = fun x => 1 + x).
+End L5.