7 files changed, 46 insertions, 5 deletions
diff --git a/test-suite/Makefile b/test-suite/Makefile
index 5d4e15b985..758374c5de 100644
--- a/test-suite/Makefile
+++ b/test-suite/Makefile
@@ -300,20 +300,20 @@ endif
 
 unit-tests/src/utest.cmx: unit-tests/src/utest.ml unit-tests/src/utest.cmi
 	$(SHOW) 'OCAMLOPT  $<'
-	$(HIDE)$(OCAMLOPT) -c -I unit-tests/src -package oUnit $<
+	$(HIDE)$(OCAMLOPT) -c -I unit-tests/src -package ounit2 $<
 unit-tests/src/utest.cmo: unit-tests/src/utest.ml unit-tests/src/utest.cmi
 	$(SHOW) 'OCAMLC  $<'
-	$(HIDE)$(OCAMLC) -c -I unit-tests/src -package oUnit $<
+	$(HIDE)$(OCAMLC) -c -I unit-tests/src -package ounit2 $<
 unit-tests/src/utest.cmi: unit-tests/src/utest.mli
 	$(SHOW) 'OCAMLC  $<'
-	$(HIDE)$(OCAMLC) -package oUnit -c $<
+	$(HIDE)$(OCAMLC) -package ounit2 -c $<
 
 unit-tests: $(UNIT_LOGFILES)
 
 # Build executable, run it to generate log file
 unit-tests/%.ml.log: unit-tests/%.ml unit-tests/src/$(UNIT_LINK)
 	$(SHOW) 'TEST      $<'
-	$(HIDE)$(OCAMLBEST) -linkall -linkpkg -package coq.toplevel,oUnit \
+	$(HIDE)$(OCAMLBEST) -linkall -linkpkg -package coq.toplevel,ounit2 \
 	     -I unit-tests/src $(UNIT_LINK) $< -o $<.test;
 	$(HIDE)./$<.test
 
diff --git a/test-suite/bugs/closed/bug_12676.v b/test-suite/bugs/closed/bug_12676.v
new file mode 100644
index 0000000000..5118ddb472
--- /dev/null
+++ b/test-suite/bugs/closed/bug_12676.v
@@ -0,0 +1,13 @@
+
+
+Definition nat_eq_dec(i j:nat) : {i=j}+{i<>j}.
+Proof.
+  pose (diseq := false).
+  decide equality.
+Defined.
+
+Set Mangle Names.
+Definition nat_eq_dec_mangle (i j:nat) : {i=j}+{i<>j}.
+Proof.
+  decide equality. (*Error: Anomaly "variable diseq unbound." ...*)
+Defined.
diff --git a/test-suite/bugs/closed/bug_12860.v b/test-suite/bugs/closed/bug_12860.v
new file mode 100644
index 0000000000..243aeceba2
--- /dev/null
+++ b/test-suite/bugs/closed/bug_12860.v
@@ -0,0 +1,10 @@
+Require Import Coq.nsatz.NsatzTactic.
+Require Import Coq.ZArith.ZArith Coq.QArith.QArith.
+
+Goal forall x y : Z, (x + y = y + x)%Z.
+  intros; nsatz.
+Qed.
+
+Goal forall x y : Q, Qeq (x + y) (y + x).
+  intros; nsatz.
+Qed.
diff --git a/test-suite/output/Notations4.out b/test-suite/output/Notations4.out
index fa03ec8193..ce51acac95 100644
--- a/test-suite/output/Notations4.out
+++ b/test-suite/output/Notations4.out
@@ -123,3 +123,5 @@ File "stdin", line 297, characters 0-30:
 Warning: Notation "_ :=: _" was already used. [notation-overridden,parsing]
 0 :=: 0
      : Prop
+fun x : nat => <{ x; (S x) }>
+     : nat -> nat
diff --git a/test-suite/output/Notations4.v b/test-suite/output/Notations4.v
index 90d8da2bec..73445bad12 100644
--- a/test-suite/output/Notations4.v
+++ b/test-suite/output/Notations4.v
@@ -298,3 +298,18 @@ Notation "x :=: y" := (x = y).
 Check (0 :=: 0).
 
 End Bug12691.
+
+Module CoercionEntryTransitivity.
+
+Declare Custom Entry com.
+Declare Custom Entry com_top.
+Notation "<{ e }>" := e (at level 0, e custom com_top at level 99).
+Notation "x ; y" :=
+         (x + y)
+           (in custom com_top at level 90, x custom com at level 90, right associativity).
+Notation "x" := x (in custom com at level 0, x constr at level 0).
+Notation "x" := x (in custom com_top at level 90, x custom com at level 90).
+
+Check fun x => <{ x ; (S x) }>.
+
+End CoercionEntryTransitivity.
diff --git a/test-suite/output/ssr_error_multiple_intro_after_case.v b/test-suite/output/ssr_error_multiple_intro_after_case.v
index 1f87966693..18997b8686 100644
--- a/test-suite/output/ssr_error_multiple_intro_after_case.v
+++ b/test-suite/output/ssr_error_multiple_intro_after_case.v
@@ -1,3 +1,4 @@
 Require Import ssreflect.
 Goal forall p : nat * nat , True.
 case => x x.
+Abort.
diff --git a/test-suite/unit-tests/.merlin.in b/test-suite/unit-tests/.merlin.in
index b2279de74e..668b431d52 100644
--- a/test-suite/unit-tests/.merlin.in
+++ b/test-suite/unit-tests/.merlin.in
@@ -3,4 +3,4 @@ REC
 S **
 B **
 
-PKG oUnit
+PKG ounit2