15 files changed, 108 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/bugs/closed/bug_11722.v b/test-suite/bugs/closed/bug_11722.v
new file mode 100644
index 0000000000..d4bd5f48b2
--- /dev/null
+++ b/test-suite/bugs/closed/bug_11722.v
@@ -0,0 +1,20 @@
+Require Import Program.
+Set Universe Polymorphism.
+
+Inductive paths@{i} (A : Type@{i}) (a : A) : A -> Type@{i} :=
+  idpath : paths A a a.
+
+Inductive nat :=
+  | O : nat
+  | S : nat -> nat.
+
+Axiom cheat : forall {A}, A.
+
+Program Definition foo@{i} : forall x : nat, paths@{i} nat x x := _.
+Next Obligation.
+  destruct x.
+  constructor.
+  apply cheat.
+Defined. (* FIXED: Universe unbound error *)
+
+Check foo@{_}.
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/misc/side-eff-leak-univs.sh b/test-suite/misc/side-eff-leak-univs.sh
new file mode 100755
index 0000000000..a0f7a8587c
--- /dev/null
+++ b/test-suite/misc/side-eff-leak-univs.sh
@@ -0,0 +1,19 @@
+#!/usr/bin/env bash
+
+set -e
+
+export COQBIN=$BIN
+export PATH=$COQBIN:$PATH
+
+cd misc/side-eff-leak-univs/
+
+coq_makefile -f _CoqProject -o Makefile
+
+make clean
+
+make src/evil_plugin.cma
+
+if make; then
+    >&2 echo 'Should have failed!'
+    exit 1
+fi
diff --git a/test-suite/misc/side-eff-leak-univs/.gitignore b/test-suite/misc/side-eff-leak-univs/.gitignore
new file mode 100644
index 0000000000..2a6a6bc68d
--- /dev/null
+++ b/test-suite/misc/side-eff-leak-univs/.gitignore
@@ -0,0 +1,2 @@
+/Makefile*
+/src/evil.ml
diff --git a/test-suite/misc/side-eff-leak-univs/_CoqProject b/test-suite/misc/side-eff-leak-univs/_CoqProject
new file mode 100644
index 0000000000..2099d862b2
--- /dev/null
+++ b/test-suite/misc/side-eff-leak-univs/_CoqProject
@@ -0,0 +1,6 @@
+-Q theories Evil
+-I src
+
+src/evil.mlg
+src/evil_plugin.mlpack
+theories/evil.v
diff --git a/test-suite/misc/side-eff-leak-univs/src/evil.mlg b/test-suite/misc/side-eff-leak-univs/src/evil.mlg
new file mode 100644
index 0000000000..d89ab887a8
--- /dev/null
+++ b/test-suite/misc/side-eff-leak-univs/src/evil.mlg
@@ -0,0 +1,13 @@
+DECLARE PLUGIN "evil_plugin"
+
+{
+open Ltac_plugin
+open Stdarg
+}
+
+TACTIC EXTEND magic
+| [ "magic" ident(i) ident(j) ] -> {
+  let open Glob_term in
+  DeclareUniv.do_constraint ~poly:false [ GType (Libnames.qualid_of_ident i), Univ.Lt, GType (Libnames.qualid_of_ident j)]; Proofview.tclUNIT()
+}
+END
diff --git a/test-suite/misc/side-eff-leak-univs/src/evil_plugin.mlpack b/test-suite/misc/side-eff-leak-univs/src/evil_plugin.mlpack
new file mode 100644
index 0000000000..6382aa69e1
--- /dev/null
+++ b/test-suite/misc/side-eff-leak-univs/src/evil_plugin.mlpack
@@ -0,0 +1 @@
+Evil
diff --git a/test-suite/misc/side-eff-leak-univs/theories/evil.v b/test-suite/misc/side-eff-leak-univs/theories/evil.v
new file mode 100644
index 0000000000..d138091fa9
--- /dev/null
+++ b/test-suite/misc/side-eff-leak-univs/theories/evil.v
@@ -0,0 +1,10 @@
+Declare ML Module "evil_plugin".
+
+Universes i j.
+
+Lemma foo@{} : Type@{j}.
+Proof.
+  magic i j; transparent_abstract exact_no_check Type@{i}.
+Defined.
+
+Definition bar : Type@{i} := Type@{j}.
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.