12 files changed, 52 insertions, 8 deletions
diff --git a/test-suite/Makefile b/test-suite/Makefile
index 6c373701cf..279f32c903 100644
--- a/test-suite/Makefile
+++ b/test-suite/Makefile
@@ -36,7 +36,8 @@ include ../Makefile.common
 # Note that this will later need an eval in shell to interpret the quotes
 ROOT='$(shell cd ..; pwd)'
 
-ifneq ($(wildcard ../_build),)
+ifneq ($(wildcard ../_build/default/config/Makefile),)
+include ../_build/default/config/Makefile
 BIN:=$(ROOT)/_build/install/default/bin/
 # COQLIB is an env variable so no quotes
 COQLIB:=$(shell cd ..; pwd)/_build/install/default/lib/coq
diff --git a/test-suite/bugs/closed/bug_10972.v b/test-suite/bugs/closed/bug_10972.v
new file mode 100644
index 0000000000..945c23c9a4
--- /dev/null
+++ b/test-suite/bugs/closed/bug_10972.v
@@ -0,0 +1,9 @@
+(* Check rewrite_strat is compatible with Ltac *)
+Require Import Coq.Setoids.Setoid.
+Module foo.
+  Definition Foo := True.
+  Ltac foo := rewrite_strat eval cbv [Foo].
+End foo.
+Goal foo.Foo.
+  foo.foo.
+Abort.
diff --git a/test-suite/bugs/closed/bug_13216.v b/test-suite/bugs/closed/bug_13216.v
new file mode 100644
index 0000000000..54a28a9c53
--- /dev/null
+++ b/test-suite/bugs/closed/bug_13216.v
@@ -0,0 +1,4 @@
+Class A.
+Declare Instance a:A.
+Inductive T `(A) := C.
+Definition f x := match x with C _ => 0 end.
diff --git a/test-suite/output/Search.out b/test-suite/output/Search.out
index 914e7f88c6..ef4c6bac93 100644
--- a/test-suite/output/Search.out
+++ b/test-suite/output/Search.out
@@ -458,3 +458,7 @@ reflexive_eq_dom_reflexive:
 B.b: B.a
 A.b: A.a
 F.L: F.P 0
+inr: forall {A B : Type}, B -> A + B
+inl: forall {A B : Type}, A -> A + B
+(use "About" for full details on the implicit arguments of inl and inr)
+f: None = 0
diff --git a/test-suite/output/Search.v b/test-suite/output/Search.v
index a5ac2cb511..2f29e1aff1 100644
--- a/test-suite/output/Search.v
+++ b/test-suite/output/Search.v
@@ -89,3 +89,10 @@ Module Bug12647.
   Search F.P.
   End Bar.
 End Bug12647.
+
+Module WithCoercions.
+  Search headconcl:(_ + _) inside Datatypes.
+  Coercion Some_nat := @Some nat.
+  Axiom f : None = 0.
+  Search (None = 0).
+End WithCoercions.
diff --git a/test-suite/output/bug_13244.out b/test-suite/output/bug_13244.out
new file mode 100644
index 0000000000..8c7d4ac776
--- /dev/null
+++ b/test-suite/output/bug_13244.out
@@ -0,0 +1,9 @@
+negbT: forall [b : bool], b = false -> ~~ b
+contra_notN: forall [P : Prop] [b : bool], (b -> P) -> ~ P -> ~~ b
+contraPN: forall [P : Prop] [b : bool], (b -> ~ P) -> P -> ~~ b
+contraNN: forall [c b : bool], (c -> b) -> ~~ b -> ~~ c
+contraL: forall [c b : bool], (c -> ~~ b) -> b -> ~~ c
+contraTN: forall [c b : bool], (c -> ~~ b) -> b -> ~~ c
+contra: forall [c b : bool], (c -> b) -> ~~ b -> ~~ c
+introN: forall [P : Prop] [b : bool], reflect P b -> ~ P -> ~~ b
+contraFN: forall [c b : bool], (c -> b) -> b = false -> ~~ c
diff --git a/test-suite/output/bug_13244.v b/test-suite/output/bug_13244.v
new file mode 100644
index 0000000000..83eaac1a35
--- /dev/null
+++ b/test-suite/output/bug_13244.v
@@ -0,0 +1,3 @@
+Require Import ssr.ssrbool.
+Set Warnings "-ssr-search-moved".
+Search headconcl:(~~ _).
diff --git a/test-suite/output/bug_13320.out b/test-suite/output/bug_13320.out
new file mode 100644
index 0000000000..97efe1da87
--- /dev/null
+++ b/test-suite/output/bug_13320.out
@@ -0,0 +1,2 @@
+The command has indeed failed with message:
+No obligations remaining
diff --git a/test-suite/output/bug_13320.v b/test-suite/output/bug_13320.v
new file mode 100644
index 0000000000..6f3c51bbe7
--- /dev/null
+++ b/test-suite/output/bug_13320.v
@@ -0,0 +1,2 @@
+(* Next Obligation should fail normally, not with an anomaly. *)
+Fail Next Obligation.
diff --git a/test-suite/success/CompatOldOldFlag.v b/test-suite/success/CompatOldOldFlag.v
deleted file mode 100644
index f408e95d2e..0000000000
--- a/test-suite/success/CompatOldOldFlag.v
+++ /dev/null
@@ -1,6 +0,0 @@
-(* -*- coq-prog-args: ("-compat" "8.10") -*- *)
-(** Check that the current-minus-three compatibility flag actually requires the relevant modules. *)
-Import Coq.Compat.Coq813.
-Import Coq.Compat.Coq812.
-Import Coq.Compat.Coq811.
-Import Coq.Compat.Coq810.
diff --git a/test-suite/success/rewrite_strat.v b/test-suite/success/rewrite_strat.v
index a6e59fdda0..98045d1162 100644
--- a/test-suite/success/rewrite_strat.v
+++ b/test-suite/success/rewrite_strat.v
@@ -51,3 +51,12 @@ Time Qed. (* 0.06 s *)
 
 Set Printing All.
 Set Printing Depth 100000.
+
+Tactic Notation "my_rewrite_strat" constr(x) := rewrite_strat topdown x.
+Tactic Notation "my_rewrite_strat2" uconstr(x) := rewrite_strat topdown x.
+Goal (forall x, S x = 0) -> 1=0.
+intro H.
+my_rewrite_strat H.
+Undo.
+my_rewrite_strat2 H.
+Abort.
diff --git a/test-suite/tools/update-compat/run.sh b/test-suite/tools/update-compat/run.sh
index 61273c4f37..7ff5571ffb 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 --master || exit $?
+dev/tools/update-compat.py --assert-unchanged --release || exit $?