8 files changed, 37 insertions, 0 deletions
diff --git a/test-suite/.csdp.cache b/test-suite/.csdp.cache
index b3bcb5b056..046cb067c5 100644
--- a/test-suite/.csdp.cache
+++ b/test-suite/.csdp.cache
diff --git a/test-suite/ide/debug_ltac.fake b/test-suite/ide/debug_ltac.fake
index aa68fad39e..38c610a5a6 100644
--- a/test-suite/ide/debug_ltac.fake
+++ b/test-suite/ide/debug_ltac.fake
@@ -1,2 +1,3 @@
+ADD { Comments "fakeide doesn't support fail as the first sentence". }
 FAILADD { Debug On. }
 ADD { Set Debug On. }
diff --git a/test-suite/ide/undo002.fake b/test-suite/ide/undo002.fake
index 5284c5d3a5..eb553f9dfa 100644
--- a/test-suite/ide/undo002.fake
+++ b/test-suite/ide/undo002.fake
@@ -3,6 +3,7 @@
 #
 # Simple backtrack by 2 before two global definitions
 #
+ADD initial { Comments "initial sentence". }
 ADD { Definition foo := 0. }
 ADD { Definition bar := 1. }
 EDIT_AT initial
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/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.
diff --git a/test-suite/success/pose.v b/test-suite/success/pose.v
new file mode 100644
index 0000000000..17007915fe
--- /dev/null
+++ b/test-suite/success/pose.v
@@ -0,0 +1,9 @@
+(* Test syntax *)
+
+Goal 0=0.
+pose proof (a := I).
+Fail clearbody a.
+epose proof (b := fun _ => eq_refl).
+Fail clearbody b.
+exact (b a).
+Qed.