6 files changed, 30 insertions, 0 deletions
diff --git a/test-suite/output/Inductive.out b/test-suite/output/Inductive.out
index 8ff571ae55..ff2556c5dc 100644
--- a/test-suite/output/Inductive.out
+++ b/test-suite/output/Inductive.out
@@ -5,3 +5,5 @@ Inductive foo (A : Type) (x : A) (y : A := x) : Prop :=  Foo : foo A x
 
 Arguments foo _%type_scope
 Arguments Foo _%type_scope
+myprod unit bool
+     : Set
diff --git a/test-suite/output/Inductive.v b/test-suite/output/Inductive.v
index 9eec9a7dad..db1276cb6c 100644
--- a/test-suite/output/Inductive.v
+++ b/test-suite/output/Inductive.v
@@ -5,3 +5,11 @@ Fail Inductive list' (A:Set) : Set :=
 (* Check printing of let-ins *)
 #[universes(template)] Inductive foo (A : Type) (x : A) (y := x) := Foo.
 Print foo.
+
+(* Check where clause *)
+Reserved Notation "x ** y" (at level 40, left associativity).
+Inductive myprod A B :=
+  mypair : A -> B -> A ** B
+  where "A ** B" := (myprod A B) (only parsing).
+
+Check unit ** bool.
diff --git a/test-suite/output/RealSyntax.out b/test-suite/output/RealSyntax.out
index 2d877bd813..2b14ca7069 100644
--- a/test-suite/output/RealSyntax.out
+++ b/test-suite/output/RealSyntax.out
@@ -2,6 +2,8 @@
      : R
 (-31)%R
      : R
+15e-1%R
+     : R
 eq_refl : 102e-2 = 102e-2
      : 102e-2 = 102e-2
 eq_refl : 102e-1 = 102e-1
diff --git a/test-suite/output/RealSyntax.v b/test-suite/output/RealSyntax.v
index cb3bce70d4..7be8b18ac8 100644
--- a/test-suite/output/RealSyntax.v
+++ b/test-suite/output/RealSyntax.v
@@ -2,6 +2,8 @@ Require Import Reals.Rdefinitions.
 Check 32%R.
 Check (-31)%R.
 
+Check 1.5_%R.
+
 Open Scope R_scope.
 
 Check (eq_refl : 1.02 = IZR 102 / IZR (Z.pow_pos 10 2)).
diff --git a/test-suite/output/bug_8206.out b/test-suite/output/bug_8206.out
new file mode 100644
index 0000000000..6015fe32f9
--- /dev/null
+++ b/test-suite/output/bug_8206.out
@@ -0,0 +1,5 @@
+File "stdin", line 11, characters 0-23:
+Error: Signature components for label homework do not match: expected type
+"forall a b : nat, bug_8206.M.add a b = bug_8206.M.add b a" but found type
+"nat -> forall b : nat, bug_8206.M.add 0 b = bug_8206.M.add b 0".
+
diff --git a/test-suite/output/bug_8206.v b/test-suite/output/bug_8206.v
new file mode 100644
index 0000000000..8d4e73dfac
--- /dev/null
+++ b/test-suite/output/bug_8206.v
@@ -0,0 +1,11 @@
+Module Type Sig.
+  Parameter add: nat -> nat -> nat.
+  Axiom homework: forall (a b: nat), add a b = add b a.
+End Sig.
+
+Module Impl.
+  Definition add(a b: nat) := plus a b.
+  Axiom homework: forall (a b: nat), add 0 b = add b 0.
+End Impl.
+
+Module M : Sig := Impl.