10 files changed, 14 insertions, 18 deletions
diff --git a/test-suite/misc/4722.sh b/test-suite/misc/4722.sh
index 86bc50b5cd..70071b9d60 100755
--- a/test-suite/misc/4722.sh
+++ b/test-suite/misc/4722.sh
@@ -4,12 +4,12 @@ set -e
 # create test files
 mkdir -p misc/4722
 ln -sf toto misc/4722/tata
-touch misc/4722.v
+touch misc/bug_4722.v
 
 # run test
-$coqtop "-R" "misc/4722" "Foo" -top Top -load-vernac-source misc/4722.v
+$coqc "-R" "misc/4722" "Foo" -top Top misc/bug_4722.v
 
 # clean up test files
 rm misc/4722/tata
 rmdir misc/4722
-rm misc/4722.v
+rm misc/bug_4722.v
diff --git a/test-suite/misc/7704.sh b/test-suite/misc/7704.sh
index 0ca2c97d24..5fc171649e 100755
--- a/test-suite/misc/7704.sh
+++ b/test-suite/misc/7704.sh
@@ -4,4 +4,4 @@ set -e
 
 export PATH=$BIN:$PATH
 
-${coqtop#"$BIN"} -compile misc/aux7704.v
+${coqc#"$BIN"} misc/aux7704.v
diff --git a/test-suite/misc/aux7704.v b/test-suite/misc/aux7704.v
index 6fdcf67684..1c95211a71 100644
--- a/test-suite/misc/aux7704.v
+++ b/test-suite/misc/aux7704.v
@@ -1,4 +1,3 @@
-
 Goal True /\ True.
 Proof.
   split.
diff --git a/test-suite/misc/deps-checksum.sh b/test-suite/misc/deps-checksum.sh
index a15a8fbee9..8523358303 100755
--- a/test-suite/misc/deps-checksum.sh
+++ b/test-suite/misc/deps-checksum.sh
@@ -3,4 +3,4 @@ rm -f misc/deps/A/*.vo misc/deps/B/*.vo
 $coqc -R misc/deps/A A misc/deps/A/A.v
 $coqc -R misc/deps/B A misc/deps/B/A.v
 $coqc -R misc/deps/B A misc/deps/B/B.v
-$coqtop -R misc/deps/B A -R misc/deps/A A -load-vernac-source misc/deps/checksum.v
+$coqc -R misc/deps/B A -R misc/deps/A A misc/deps/checksum.v
diff --git a/test-suite/misc/deps-order.sh b/test-suite/misc/deps-order.sh
index 6bb2ba2da0..551515b0d6 100755
--- a/test-suite/misc/deps-order.sh
+++ b/test-suite/misc/deps-order.sh
@@ -10,12 +10,12 @@ R=$?
 times
 $coqc -R misc/deps/lib lib misc/deps/lib/foo.v 2>&1
 $coqc -R misc/deps/lib lib -R misc/deps/client client misc/deps/client/foo.v 2>&1
-$coqtop -R misc/deps/lib lib -R misc/deps/client client -load-vernac-source misc/deps/client/bar.v 2>&1
+$coqc -R misc/deps/lib lib -R misc/deps/client client misc/deps/client/bar.v 2>&1
 S=$?
 if [ $R = 0 ] && [ $S = 0 ]; then
-    printf "coqdep and coqtop agree\n"
+    printf "coqdep and coqc agree\n"
     exit 0
 else
-    printf "coqdep and coqtop disagree\n"
+    printf "coqdep and coqc disagree\n"
     exit 1
 fi
diff --git a/test-suite/misc/deps-utf8.sh b/test-suite/misc/deps-utf8.sh
index acb45b2292..af69370ce4 100755
--- a/test-suite/misc/deps-utf8.sh
+++ b/test-suite/misc/deps-utf8.sh
@@ -8,7 +8,7 @@ rm -f misc/deps/théorèmes/*.v
 tmpoutput=$(mktemp /tmp/coqcheck.XXXXXX)
 $coqc -R misc/deps AlphaBêta misc/deps/αβ/γδ.v
 R=$?
-$coqtop -R misc/deps AlphaBêta -load-vernac-source misc/deps/αβ/εζ.v
+$coqc -R misc/deps AlphaBêta misc/deps/αβ/εζ.v
 S=$?
 if [ $R = 0 ] && [ $S = 0 ]; then
     exit 0
diff --git a/test-suite/misc/exitstatus.sh b/test-suite/misc/exitstatus.sh
index a327f4248b..afc415b2da 100755
--- a/test-suite/misc/exitstatus.sh
+++ b/test-suite/misc/exitstatus.sh
@@ -1,8 +1,5 @@
 #!/bin/sh
-$coqtop -load-vernac-source misc/exitstatus/illtyped.v
-N=$?
 $coqc misc/exitstatus/illtyped.v
 P=$?
-printf "On ill-typed input, coqtop returned %s.\n" "$N"
 printf "On ill-typed input, coqc returned %s.\n" "$P"
-if [ $N = 1 ] && [ $P = 1 ]; then exit 0; else exit 1; fi
+if [ $P = 1 ]; then exit 0; else exit 1; fi
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/misc/poly-capture-global-univs/src/evilImpl.ml b/test-suite/misc/poly-capture-global-univs/src/evilImpl.ml
index 047f4cd080..f5043db099 100644
--- a/test-suite/misc/poly-capture-global-univs/src/evilImpl.ml
+++ b/test-suite/misc/poly-capture-global-univs/src/evilImpl.ml
@@ -9,13 +9,13 @@ let evil t f =
   let u = Level.var 0 in
   let tu = mkType (Universe.make u) in
   let te = Declare.definition_entry
-      ~univs:(Monomorphic_const_entry (ContextSet.singleton u)) tu
+      ~univs:(Monomorphic_entry (ContextSet.singleton u)) tu
   in
   let tc = Declare.declare_constant t (DefinitionEntry te, k) in
   let tc = mkConst tc in
 
   let fe = Declare.definition_entry
-      ~univs:(Polymorphic_const_entry ([|Anonymous|], UContext.make (Instance.of_array [|u|],Constraint.empty)))
+      ~univs:(Polymorphic_entry ([|Anonymous|], UContext.make (Instance.of_array [|u|],Constraint.empty)))
       ~types:(Term.mkArrow tc tu)
       (mkLambda (Name.Name (Id.of_string "x"), tc, mkRel 1))
   in
diff --git a/test-suite/misc/universes/dune b/test-suite/misc/universes/dune
index 58bba300d2..0772f95604 100644
--- a/test-suite/misc/universes/dune
+++ b/test-suite/misc/universes/dune
@@ -5,4 +5,4 @@
    (source_tree ../../../plugins))
  (action
    (with-outputs-to all_stdlib.v
-    (run ./build_all_stdlib.sh))))
+    (bash "./build_all_stdlib.sh"))))