11 files changed, 117 insertions, 7 deletions
diff --git a/test-suite/bugs/closed/bug_10504.v b/test-suite/bugs/closed/bug_10504.v
new file mode 100644
index 0000000000..6e66a6a90a
--- /dev/null
+++ b/test-suite/bugs/closed/bug_10504.v
@@ -0,0 +1,14 @@
+Inductive any_list {A} :=
+| nil : @any_list A
+| cons : forall X, A -> @any_list X -> @any_list A.
+
+Arguments nil {A}.
+Arguments cons {A X}.
+
+Notation "[]" := (@nil Type).
+Notation "hd :: tl" := (cons hd tl).
+
+Definition xs := true :: 2137 :: false :: 0 :: [].
+Fail Definition ys := xs :: xs.
+
+(* Goal ys = ys. produced an anomaly "Unable to handle arbitrary u+k <= v constraints" *)
diff --git a/test-suite/bugs/closed/bug_11039.v b/test-suite/bugs/closed/bug_11039.v
new file mode 100644
index 0000000000..f02a3ef177
--- /dev/null
+++ b/test-suite/bugs/closed/bug_11039.v
@@ -0,0 +1,26 @@
+(* this bug was a proof of False *)
+
+(* when we require template poly Coq recognizes that it's not allowed *)
+Fail #[universes(template)]
+  Inductive foo@{i} (A:Type@{i}) : Type@{i+1} := bar (X:Type@{i}) : foo A.
+
+(* variants with letin *)
+Fail #[universes(template)]
+ Inductive foo@{i}  (T:=Type@{i}:Type@{i+1}) (A:Type@{i}) : Type@{i+1} := bar (X:T) : foo A.
+
+Fail #[universes(template)]
+ Record foo@{i}  (T:=Type@{i}:Type@{i+1}) (A:Type@{i}) : Type@{i+1} := bar { X:T }.
+
+
+(* no implicit template poly, no explicit universe annotations *)
+Inductive foo (A:Type) := bar X : foo X -> foo A | nonempty.
+Arguments nonempty {_}.
+
+Fail Check foo nat : Type@{foo.u0}.
+(* template poly didn't activate *)
+
+Definition U := Type.
+Definition A : U := foo nat.
+
+Fail Definition down : U -> A := fun u => bar nat u nonempty.
+(* this is the one where it's important that it fails *)
diff --git a/test-suite/bugs/closed/bug_11161.v b/test-suite/bugs/closed/bug_11161.v
new file mode 100644
index 0000000000..22a075e096
--- /dev/null
+++ b/test-suite/bugs/closed/bug_11161.v
@@ -0,0 +1,10 @@
+(* Ensure that evars are properly normalized in the instance path.
+   Problems with this can cause eg #11161. *)
+
+Class Foo (n:nat) := {x : bool}.
+
+Instance bar n : Foo n. Admitted.
+
+Instance bar' n : Foo n. split. abstract exact true. Qed.
+
+Instance bar'' n : Foo n. split. abstract exact true. Defined.
diff --git a/test-suite/complexity/pattern.v b/test-suite/complexity/pattern.v
new file mode 100644
index 0000000000..fb5bf5a00b
--- /dev/null
+++ b/test-suite/complexity/pattern.v
@@ -0,0 +1,38 @@
+(** Testing the performance of [pattern].  For not regressing on COQBUG(https://github.com/coq/coq/issues/11150) and COQBUG(https://github.com/coq/coq/issues/6502) *)
+(* Expected time < 0.75s *)
+(* reference: 0.673s after adjustment *)
+Definition Let_In {A P} (v : A) (f : forall x : A, P x) : P v
+:= let x := v in f x.
+
+Fixpoint big (a : nat) (sz : nat) : nat
+  := match sz with
+     | O => a
+     | S sz' => Let_In (a * a) (fun a' => big a' sz')
+     end.
+
+Ltac do_time n :=
+  try (
+      once (assert (exists e, e = big 1 n);
+            [ lazy -[big]; (*match goal with |- ?G => idtac G end;*) lazy [big];
+              time pattern Nat.mul, S, O, (@Let_In nat (fun _ => nat))
+            | ]);
+      fail).
+
+Ltac do_time_to n :=
+  lazymatch (eval vm_compute in n) with
+  | O => idtac
+  | ?n' => do_time_to (Nat.div2 n'); idtac n'; do_time n'
+  end.
+
+Local Set Warnings "-abstract-large-number".
+
+(* Don't spend lots of time printing *)
+Notation hide := (_ = _).
+
+Goal True.
+Proof.
+  (* do_time_to 16384. *) (* should be linear, not quadratic *)
+  assert (exists e, e = big 1 16384).
+  lazy -[big]; (*match goal with |- ?G => idtac G end;*) lazy [big].
+  Timeout 15 Time pattern Nat.mul, S, O, (@Let_In nat (fun _ => nat)).
+Abort.
diff --git a/test-suite/output/Notations4.out b/test-suite/output/Notations4.out
index ba4ac5a8f9..32120a9674 100644
--- a/test-suite/output/Notations4.out
+++ b/test-suite/output/Notations4.out
@@ -59,3 +59,5 @@ where
       |- Type] (pat, p0, p cannot be used)
 fun '{| |} => true
      : R -> bool
+b = a
+     : Prop
diff --git a/test-suite/output/Notations4.v b/test-suite/output/Notations4.v
index 4b9d0abd95..d3433949d1 100644
--- a/test-suite/output/Notations4.v
+++ b/test-suite/output/Notations4.v
@@ -140,3 +140,17 @@ Record R := { n : nat }.
 Check fun '{|n:=x|} => true.
 
 End EmptyRecordSyntax.
+
+Module L.
+
+(* Testing regression #11053 *)
+
+Section Test.
+Variables (A B : Type) (a : A) (b : B).
+Variable c : A -> B.
+Coercion c : A >-> B.
+Notation COERCION := (c).
+Check b = a.
+End Test.
+
+End L.
diff --git a/test-suite/success/CompatCurrentFlag.v b/test-suite/success/CompatCurrentFlag.v
index fd6101bf89..c86548440b 100644
--- a/test-suite/success/CompatCurrentFlag.v
+++ b/test-suite/success/CompatCurrentFlag.v
@@ -1,3 +1,3 @@
-(* -*- coq-prog-args: ("-compat" "8.11") -*- *)
+(* -*- coq-prog-args: ("-compat" "8.12") -*- *)
 (** Check that the current compatibility flag actually requires the relevant modules. *)
-Import Coq.Compat.Coq811.
+Import Coq.Compat.Coq812.
diff --git a/test-suite/success/CompatOldFlag.v b/test-suite/success/CompatOldFlag.v
index f774cef44f..a1c1209db6 100644
--- a/test-suite/success/CompatOldFlag.v
+++ b/test-suite/success/CompatOldFlag.v
@@ -1,5 +1,5 @@
-(* -*- coq-prog-args: ("-compat" "8.9") -*- *)
+(* -*- coq-prog-args: ("-compat" "8.10") -*- *)
 (** Check that the current-minus-two compatibility flag actually requires the relevant modules. *)
+Import Coq.Compat.Coq812.
 Import Coq.Compat.Coq811.
 Import Coq.Compat.Coq810.
-Import Coq.Compat.Coq89.
diff --git a/test-suite/success/CompatOldOldFlag.v b/test-suite/success/CompatOldOldFlag.v
new file mode 100644
index 0000000000..dd259988ac
--- /dev/null
+++ b/test-suite/success/CompatOldOldFlag.v
@@ -0,0 +1,6 @@
+(* -*- coq-prog-args: ("-compat" "8.9") -*- *)
+(** Check that the current-minus-three compatibility flag actually requires the relevant modules. *)
+Import Coq.Compat.Coq812.
+Import Coq.Compat.Coq811.
+Import Coq.Compat.Coq810.
+Import Coq.Compat.Coq89.
diff --git a/test-suite/success/CompatPreviousFlag.v b/test-suite/success/CompatPreviousFlag.v
index 1c5ccc1a92..00f4747e3e 100644
--- a/test-suite/success/CompatPreviousFlag.v
+++ b/test-suite/success/CompatPreviousFlag.v
@@ -1,4 +1,4 @@
-(* -*- coq-prog-args: ("-compat" "8.10") -*- *)
+(* -*- coq-prog-args: ("-compat" "8.11") -*- *)
 (** Check that the current-minus-one compatibility flag actually requires the relevant modules. *)
+Import Coq.Compat.Coq812.
 Import Coq.Compat.Coq811.
-Import Coq.Compat.Coq810.
diff --git a/test-suite/tools/update-compat/run.sh b/test-suite/tools/update-compat/run.sh
index 7ff5571ffb..61273c4f37 100755
--- a/test-suite/tools/update-compat/run.sh
+++ b/test-suite/tools/update-compat/run.sh
@@ -6,4 +6,4 @@ SCRIPT_DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" >/dev/null && pwd )"
 # we assume that the script lives in test-suite/tools/update-compat/,
 # and that update-compat.py lives in dev/tools/
 cd "${SCRIPT_DIR}/../../.."
-dev/tools/update-compat.py --assert-unchanged --release || exit $?
+dev/tools/update-compat.py --assert-unchanged --master || exit $?