6 files changed, 34 insertions, 0 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/Notations3.out b/test-suite/output/Notations3.out
index 5ab616160a..d32cf67e28 100644
--- a/test-suite/output/Notations3.out
+++ b/test-suite/output/Notations3.out
@@ -246,3 +246,9 @@ Notation
   ============================
   ##@%
    ^^^
+myfoo01 tt
+     : nat
+myfoo01 tt
+     : nat
+myfoo01 tt
+     : nat
diff --git a/test-suite/output/Notations3.v b/test-suite/output/Notations3.v
index 876aaa3944..180e8d337e 100644
--- a/test-suite/output/Notations3.v
+++ b/test-suite/output/Notations3.v
@@ -399,3 +399,14 @@ 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.