13 files changed, 170 insertions, 11 deletions
diff --git a/test-suite/output/BadOptionValueType.out b/test-suite/output/BadOptionValueType.out
new file mode 100644
index 0000000000..34d8518a75
--- /dev/null
+++ b/test-suite/output/BadOptionValueType.out
@@ -0,0 +1,8 @@
+The command has indeed failed with message:
+Bad type of value for this option: expected int, got string.
+The command has indeed failed with message:
+Bad type of value for this option: expected bool, got string.
+The command has indeed failed with message:
+Bad type of value for this option: expected bool, got int.
+The command has indeed failed with message:
+Bad type of value for this option: expected bool, got int.
diff --git a/test-suite/output/BadOptionValueType.v b/test-suite/output/BadOptionValueType.v
new file mode 100644
index 0000000000..b61c3757ba
--- /dev/null
+++ b/test-suite/output/BadOptionValueType.v
@@ -0,0 +1,4 @@
+Fail Set Default Timeout "2".
+Fail Set Debug Eauto "yes".
+Fail Set Debug Eauto 1.
+Fail Set Implicit Arguments 1.
diff --git a/test-suite/output/Cases.out b/test-suite/output/Cases.out
index 419dcadb4c..dfab400baa 100644
--- a/test-suite/output/Cases.out
+++ b/test-suite/output/Cases.out
@@ -169,3 +169,5 @@ fun x : K => match x with
              | _ => 2
              end
      : K -> nat
+The command has indeed failed with message:
+Pattern "S _, _" is redundant in this clause.
diff --git a/test-suite/output/Cases.v b/test-suite/output/Cases.v
index 4740c009a4..e4fa7044e7 100644
--- a/test-suite/output/Cases.v
+++ b/test-suite/output/Cases.v
@@ -217,3 +217,6 @@ Check fun x => match x with a3 | a4 => 3 | _ => 2 end.
 Check fun x => match x with a3 => 3 | a2 | a1 => 4 | _ => 2 end.
 Check fun x => match x with a4 => 3 | a2 | a1 => 4 | _ => 2 end.
 Check fun x => match x with a3 | a4 | a1 => 3 | _ => 2 end.
+
+(* Test redundant clause within a disjunctive pattern *)
+Fail Check fun n m => match n, m with 0, 0 | _, S _ | S 0, _ | S (S _ | _), _ => false end.
diff --git a/test-suite/output/Deprecation.out b/test-suite/output/Deprecation.out
new file mode 100644
index 0000000000..7e290847c1
--- /dev/null
+++ b/test-suite/output/Deprecation.out
@@ -0,0 +1,3 @@
+File "stdin", line 5, characters 0-3:
+Warning: Tactic foo is deprecated since X.Y. Use idtac instead.
+[deprecated-tactic,deprecated]
diff --git a/test-suite/output/Deprecation.v b/test-suite/output/Deprecation.v
new file mode 100644
index 0000000000..04d5eb3d4a
--- /dev/null
+++ b/test-suite/output/Deprecation.v
@@ -0,0 +1,6 @@
+#[deprecated(since = "X.Y", note = "Use idtac instead.")]
+ Ltac foo := idtac.
+
+Goal True.
+foo.
+Abort.
diff --git a/test-suite/output/Notations3.out b/test-suite/output/Notations3.out
index 996af59270..d32cf67e28 100644
--- a/test-suite/output/Notations3.out
+++ b/test-suite/output/Notations3.out
@@ -241,3 +241,14 @@ Notation
 Notation
 "( x , y , .. , z )" := pair .. (pair x y) .. z : core_scope
 (default interpretation)
+1 subgoal
+  
+  ============================
+  ##@%
+   ^^^
+myfoo01 tt
+     : nat
+myfoo01 tt
+     : nat
+myfoo01 tt
+     : nat
diff --git a/test-suite/output/Notations3.v b/test-suite/output/Notations3.v
index 3cf0c913f7..180e8d337e 100644
--- a/test-suite/output/Notations3.v
+++ b/test-suite/output/Notations3.v
@@ -385,3 +385,28 @@ Module LocateNotations.
 Locate "exists".
 Locate "( _ , _ , .. , _ )".
 End LocateNotations.
+
+Module Issue7731.
+
+Axiom (P : nat -> Prop).
+Parameter (X : nat).
+Notation "## @ E ^^^" := (P E) (at level 20, E at level 1, format "'[ ' ## '/' @ E '/' ^^^ ']'").
+Notation "%" := X.
+
+Set Printing Width 7.
+Goal ## @ % ^^^.
+Show.
+Abort.
+
+End Issue7731.
+
+Module Issue8126.
+
+Definition myfoo (x : nat) (y : nat) (z : unit) := y.
+Notation myfoo0 := (@myfoo 0).
+Notation myfoo01 := (@myfoo0 1).
+Check myfoo 0 1 tt. (* was printing [myfoo0 1 HI], but should print [myfoo01 HI]  *)
+Check myfoo0 1 tt. (* was printing [myfoo0 1 HI], but should print [myfoo01 HI]  *)
+Check myfoo01 tt. (* was printing [myfoo0 1 HI], but should print [myfoo01 HI]  *)
+
+End Issue8126.
diff --git a/test-suite/output/Notations4.out b/test-suite/output/Notations4.out
new file mode 100644
index 0000000000..cef7d1a702
--- /dev/null
+++ b/test-suite/output/Notations4.out
@@ -0,0 +1,17 @@
+[< 0 > + < 1 > * < 2 >]
+     : nat
+[<< # 0 >>]
+     : option nat
+[1 {f 1}]
+     : Expr
+fun (x : nat) (y z : Expr) => [1 + y z + {f x}]
+     : nat -> Expr -> Expr -> Expr
+fun e : Expr =>
+match e with
+| [x y + z] => [x + y z]
+| [1 + 1] => [1]
+| _ => [e + e]
+end
+     : Expr -> Expr
+[(1 + 1)]
+     : Expr
diff --git a/test-suite/output/Notations4.v b/test-suite/output/Notations4.v
new file mode 100644
index 0000000000..9738ce5a5e
--- /dev/null
+++ b/test-suite/output/Notations4.v
@@ -0,0 +1,68 @@
+(* An example with constr subentries *)
+
+Module A.
+
+Declare Custom Entry myconstr.
+
+Notation "[ x ]" := x (x custom myconstr at level 6).
+Notation "x + y" := (Nat.add x y) (in custom myconstr at level 5).
+Notation "x * y" := (Nat.mul x y) (in custom myconstr at level 4).
+Notation "< x >" := x (in custom myconstr at level 3, x constr at level 10).
+Check [ < 0 > + < 1 > * < 2 >].
+
+Declare Custom Entry anotherconstr.
+
+Notation "[ x ]" := x (x custom myconstr at level 6).
+Notation "<< x >>" := x (in custom myconstr at level 3, x custom anotherconstr at level 10).
+Notation "# x" := (Some x) (in custom anotherconstr at level 8, x constr at level 9).
+Check [ << # 0 >> ].
+
+End A.
+
+Module B.
+
+Inductive Expr :=
+ | Mul : Expr -> Expr -> Expr
+ | Add : Expr -> Expr -> Expr
+ | One : Expr.
+
+Declare Custom Entry expr.
+Notation "[ expr ]" := expr (expr custom expr at level 2).
+Notation "1" := One (in custom expr at level 0).
+Notation "x y" := (Mul x y) (in custom expr at level 1, left associativity).
+Notation "x + y" := (Add x y) (in custom expr at level 2, left associativity).
+Notation "( x )" := x (in custom expr at level 0, x at level 2).
+Notation "{ x }" := x (in custom expr at level 0, x constr).
+Notation "x" := x (in custom expr at level 0, x ident).
+
+Axiom f : nat -> Expr.
+Check [1 {f 1}].
+Check fun x y z => [1 + y z + {f x}].
+Check fun e => match e with
+| [x y + z] => [x + y z]
+| [1 + 1] => [1]
+| y => [y + e]
+end.
+
+End B.
+
+Module C.
+
+Inductive Expr :=
+ | Add : Expr -> Expr -> Expr
+ | One : Expr.
+
+Declare Custom Entry expr.
+Notation "[ expr ]" := expr (expr custom expr at level 1).
+Notation "1" := One (in custom expr at level 0).
+Notation "x + y" := (Add x y) (in custom expr at level 2, left associativity).
+Notation "( x )" := x (in custom expr at level 0, x at level 2).
+
+(* Check the use of a two-steps coercion from constr to expr 1 then
+   from expr 0 to expr 2 (note that camlp5 parsing is more tolerant
+   and does not require parentheses to parse from level 2 while at
+   level 1) *)
+
+Check [1 + 1].
+
+End C.
diff --git a/test-suite/output/RecordMissingField.out b/test-suite/output/RecordMissingField.out
new file mode 100644
index 0000000000..7c80a6065f
--- /dev/null
+++ b/test-suite/output/RecordMissingField.out
@@ -0,0 +1,4 @@
+File "stdin", line 8, characters 5-22:
+Error: Cannot infer field y2p of record point2d in environment:
+p : point2d
+
diff --git a/test-suite/output/RecordMissingField.v b/test-suite/output/RecordMissingField.v
new file mode 100644
index 0000000000..84f1748fa0
--- /dev/null
+++ b/test-suite/output/RecordMissingField.v
@@ -0,0 +1,8 @@
+(** Check for error message when missing a record field. Error message
+should contain missing field, and the inferred type of the record **)
+
+Record point2d := mkPoint { x2p: nat; y2p: nat }.
+
+
+Definition increment_x (p: point2d) : point2d :=
+  {| x2p := x2p p + 1; |}.
diff --git a/test-suite/output/ssr_explain_match.out b/test-suite/output/ssr_explain_match.out
index fa2393b910..32cfb354bf 100644
--- a/test-suite/output/ssr_explain_match.out
+++ b/test-suite/output/ssr_explain_match.out
@@ -1,35 +1,35 @@
 File "stdin", line 12, characters 0-61:
-Warning: Notation _ - _ was already used in scope nat_scope.
+Warning: Notation "_ - _" was already used in scope nat_scope.
 [notation-overridden,parsing]
 File "stdin", line 12, characters 0-61:
-Warning: Notation _ <= _ was already used in scope nat_scope.
+Warning: Notation "_ <= _" was already used in scope nat_scope.
 [notation-overridden,parsing]
 File "stdin", line 12, characters 0-61:
-Warning: Notation _ < _ was already used in scope nat_scope.
+Warning: Notation "_ < _" was already used in scope nat_scope.
 [notation-overridden,parsing]
 File "stdin", line 12, characters 0-61:
-Warning: Notation _ >= _ was already used in scope nat_scope.
+Warning: Notation "_ >= _" was already used in scope nat_scope.
 [notation-overridden,parsing]
 File "stdin", line 12, characters 0-61:
-Warning: Notation _ > _ was already used in scope nat_scope.
+Warning: Notation "_ > _" was already used in scope nat_scope.
 [notation-overridden,parsing]
 File "stdin", line 12, characters 0-61:
-Warning: Notation _ <= _ <= _ was already used in scope nat_scope.
+Warning: Notation "_ <= _ <= _" was already used in scope nat_scope.
 [notation-overridden,parsing]
 File "stdin", line 12, characters 0-61:
-Warning: Notation _ < _ <= _ was already used in scope nat_scope.
+Warning: Notation "_ < _ <= _" was already used in scope nat_scope.
 [notation-overridden,parsing]
 File "stdin", line 12, characters 0-61:
-Warning: Notation _ <= _ < _ was already used in scope nat_scope.
+Warning: Notation "_ <= _ < _" was already used in scope nat_scope.
 [notation-overridden,parsing]
 File "stdin", line 12, characters 0-61:
-Warning: Notation _ < _ < _ was already used in scope nat_scope.
+Warning: Notation "_ < _ < _" was already used in scope nat_scope.
 [notation-overridden,parsing]
 File "stdin", line 12, characters 0-61:
-Warning: Notation _ + _ was already used in scope nat_scope.
+Warning: Notation "_ + _" was already used in scope nat_scope.
 [notation-overridden,parsing]
 File "stdin", line 12, characters 0-61:
-Warning: Notation _ * _ was already used in scope nat_scope.
+Warning: Notation "_ * _" was already used in scope nat_scope.
 [notation-overridden,parsing]
 BEGIN INSTANCES
 instance: (x + y + z) matches: (x + y + z)