9 files changed, 37 insertions, 13 deletions
diff --git a/test-suite/Makefile b/test-suite/Makefile
index 68acb6f04d..03bfc5ffac 100644
--- a/test-suite/Makefile
+++ b/test-suite/Makefile
@@ -260,6 +260,7 @@ ifeq ($(LOCAL),true)
 endif
 
 OCAMLOPT := $(OCAMLFIND) opt $(CAMLFLAGS)
+OCAMLC := $(OCAMLFIND) ocamlc $(CAMLFLAGS)
 
 # ML files from unit-test framework, not containing tests
 UNIT_SRCFILES:=$(shell find ./unit-tests/src -name *.ml)
@@ -267,24 +268,31 @@ UNIT_ALLMLFILES:=$(shell find ./unit-tests -name *.ml)
 UNIT_MLFILES:=$(filter-out $(UNIT_SRCFILES),$(UNIT_ALLMLFILES))
 UNIT_LOGFILES:=$(patsubst %.ml,%.ml.log,$(UNIT_MLFILES))
 
-UNIT_CMXS=utest.cmx
+ifneq ($(BEST),opt)
+UNIT_LINK:=utest.cmo
+OCAMLBEST:=$(OCAMLC)
+else
+UNIT_LINK:=utest.cmx
+OCAMLBEST:=$(OCAMLOPT)
+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 $<
+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 $<
 unit-tests/src/utest.cmi: unit-tests/src/utest.mli
-	$(SHOW) 'OCAMLOPT  $<'
-	$(HIDE)$(OCAMLOPT) -package oUnit $<
-
-$(UNIT_LOGFILES): unit-tests/src/utest.cmx
+	$(SHOW) 'OCAMLC  $<'
+	$(HIDE)$(OCAMLC) -package oUnit -c $<
 
 unit-tests: $(UNIT_LOGFILES)
 
 # Build executable, run it to generate log file
-unit-tests/%.ml.log: unit-tests/%.ml
+unit-tests/%.ml.log: unit-tests/%.ml unit-tests/src/$(UNIT_LINK)
 	$(SHOW) 'TEST      $<'
-	$(HIDE)$(OCAMLOPT) -linkall -linkpkg -package coq.toplevel,oUnit \
-	     -I unit-tests/src $(UNIT_CMXS) $< -o $<.test;
+	$(HIDE)$(OCAMLBEST) -linkall -linkpkg -package coq.toplevel,oUnit \
+	     -I unit-tests/src $(UNIT_LINK) $< -o $<.test;
 	$(HIDE)./$<.test
 
 #######################################################################
diff --git a/test-suite/bugs/closed/HoTT_coq_056.v b/test-suite/bugs/closed/HoTT_coq_056.v
index b80e0bb0e4..e28314cada 100644
--- a/test-suite/bugs/closed/HoTT_coq_056.v
+++ b/test-suite/bugs/closed/HoTT_coq_056.v
@@ -82,7 +82,7 @@ Notation "F ^op" := (OppositeFunctor F) : functor_scope.
 Definition FunctorProduct' C D C' D' (F : Functor C D) (F' : Functor C' D') : Functor (C * C') (D * D')
   := admit.
 
-Global Class FunctorApplicationInterpretable
+Class FunctorApplicationInterpretable
        {C D} (F : Functor C D)
        {argsT : Type} (args : argsT)
        {T : Type} (rtn : T)
diff --git a/test-suite/bugs/closed/HoTT_coq_061.v b/test-suite/bugs/closed/HoTT_coq_061.v
index 19551dc92e..72bc04e05e 100644
--- a/test-suite/bugs/closed/HoTT_coq_061.v
+++ b/test-suite/bugs/closed/HoTT_coq_061.v
@@ -96,7 +96,7 @@ Definition NTWhiskerR C D E (F F' : Functor D E) (T : NaturalTransformation F F'
   := Build_NaturalTransformation (F o G) (F' o G)
                                  (fun c => T (G c))
                                  admit.
-Global Class NTC_Composable A B (a : A) (b : B) (T : Type) (term : T) := {}.
+Class NTC_Composable A B (a : A) (b : B) (T : Type) (term : T) := {}.
 
 Definition NTC_Composable_term `{@NTC_Composable A B a b T term} := term.
 Notation "T 'o' U"
diff --git a/test-suite/bugs/closed/HoTT_coq_120.v b/test-suite/bugs/closed/HoTT_coq_120.v
index a80d075f69..cd6539b51c 100644
--- a/test-suite/bugs/closed/HoTT_coq_120.v
+++ b/test-suite/bugs/closed/HoTT_coq_120.v
@@ -89,7 +89,7 @@ Definition set_cat : PreCategory
   := @Build_PreCategory hSet
                         (fun x y => forall _ : x, y)%core
                         (fun _ _ _ f g x => f (g x))%core.
-Local Inductive minus1Trunc (A :Type) : Type := min1 : A -> minus1Trunc A.
+Inductive minus1Trunc (A :Type) : Type := min1 : A -> minus1Trunc A.
 Instance minus1Trunc_is_prop {A : Type} : IsHProp (minus1Trunc A) | 0. Admitted.
 Definition hexists {X} (P:X->Type):Type:= minus1Trunc (sigT  P).
 Definition isepi {X Y} `(f:X->Y) := forall Z: hSet,
diff --git a/test-suite/bugs/closed/bug_3427.v b/test-suite/bugs/closed/bug_3427.v
index 317efb0b32..f00d2fcf09 100644
--- a/test-suite/bugs/closed/bug_3427.v
+++ b/test-suite/bugs/closed/bug_3427.v
@@ -146,7 +146,7 @@ Section Univalence.
     := (equiv_path A B)^-1 f.
 End Univalence.
 
-Local Inductive minus1Trunc (A :Type) : Type :=
+Inductive minus1Trunc (A :Type) : Type :=
   min1 : A -> minus1Trunc A.
 
 Instance minus1Trunc_is_prop {A : Type} : IsHProp (minus1Trunc A) | 0.
diff --git a/test-suite/bugs/closed/bug_7795.v b/test-suite/bugs/closed/bug_7795.v
index 5db0f81cc5..5f9d42f5f7 100644
--- a/test-suite/bugs/closed/bug_7795.v
+++ b/test-suite/bugs/closed/bug_7795.v
@@ -52,6 +52,8 @@ Definition hh:
          false = true.
 Admitted.
 
+Require Import Program.
+
 Set Program Mode. (* removing this line prevents the bug *)
 Obligation Tactic := repeat t_base.
 
diff --git a/test-suite/bugs/closed/bug_9494.v b/test-suite/bugs/closed/bug_9494.v
new file mode 100644
index 0000000000..a0b8383d16
--- /dev/null
+++ b/test-suite/bugs/closed/bug_9494.v
@@ -0,0 +1,10 @@
+Lemma foo (a : nat) : True.
+Proof.
+destruct a eqn:n; exact I.
+Qed.
+
+Set Mangle Names.
+Lemma foo2 (a : nat) : True.
+Proof.
+let N := fresh in destruct a eqn:N; exact I.
+Qed.
diff --git a/test-suite/misc/poly-capture-global-univs.sh b/test-suite/misc/poly-capture-global-univs.sh
index e066ac039b..39d20fd524 100755
--- a/test-suite/misc/poly-capture-global-univs.sh
+++ b/test-suite/misc/poly-capture-global-univs.sh
@@ -11,7 +11,7 @@ coq_makefile -f _CoqProject -o Makefile
 
 make clean
 
-make src/evil_plugin.cmxs
+make src/evil_plugin.cma
 
 if make; then
     >&2 echo 'Should have failed!'
diff --git a/test-suite/stm/arg_filter_1.v b/test-suite/stm/arg_filter_1.v
new file mode 100644
index 0000000000..1cf66d6b43
--- /dev/null
+++ b/test-suite/stm/arg_filter_1.v
@@ -0,0 +1,4 @@
+(* coq-prog-args: ("-async-proofs-tac-j" "1") *)
+
+Lemma foo : True.
+Proof. now auto. Qed.