15 files changed, 73 insertions, 25 deletions
diff --git a/test-suite/coq-makefile/coqdoc1/run.sh b/test-suite/coq-makefile/coqdoc1/run.sh
index d6bb52bb4..e8291c89d 100755
--- a/test-suite/coq-makefile/coqdoc1/run.sh
+++ b/test-suite/coq-makefile/coqdoc1/run.sh
@@ -15,9 +15,7 @@ make install-doc DSTROOT="$PWD/tmp"
 sort -u > desired <<EOT
 .
 ./test
-./test/test_plugin.cma
 ./test/test_plugin.cmi
-./test/test_plugin.cmo
 ./test/test_plugin.cmx
 ./test/test_plugin.cmxs
 ./test/test.glob
diff --git a/test-suite/coq-makefile/coqdoc2/run.sh b/test-suite/coq-makefile/coqdoc2/run.sh
index d6bb52bb4..e8291c89d 100755
--- a/test-suite/coq-makefile/coqdoc2/run.sh
+++ b/test-suite/coq-makefile/coqdoc2/run.sh
@@ -15,9 +15,7 @@ make install-doc DSTROOT="$PWD/tmp"
 sort -u > desired <<EOT
 .
 ./test
-./test/test_plugin.cma
 ./test/test_plugin.cmi
-./test/test_plugin.cmo
 ./test/test_plugin.cmx
 ./test/test_plugin.cmxs
 ./test/test.glob
diff --git a/test-suite/coq-makefile/mlpack1/run.sh b/test-suite/coq-makefile/mlpack1/run.sh
index f6fb3bcb4..10a200dde 100755
--- a/test-suite/coq-makefile/mlpack1/run.sh
+++ b/test-suite/coq-makefile/mlpack1/run.sh
@@ -15,9 +15,7 @@ sort > desired <<EOT
 .
 ./test
 ./test/test.glob
-./test/test_plugin.cma
 ./test/test_plugin.cmi
-./test/test_plugin.cmo
 ./test/test_plugin.cmx
 ./test/test_plugin.cmxs
 ./test/test.v
diff --git a/test-suite/coq-makefile/mlpack2/run.sh b/test-suite/coq-makefile/mlpack2/run.sh
index f6fb3bcb4..10a200dde 100755
--- a/test-suite/coq-makefile/mlpack2/run.sh
+++ b/test-suite/coq-makefile/mlpack2/run.sh
@@ -15,9 +15,7 @@ sort > desired <<EOT
 .
 ./test
 ./test/test.glob
-./test/test_plugin.cma
 ./test/test_plugin.cmi
-./test/test_plugin.cmo
 ./test/test_plugin.cmx
 ./test/test_plugin.cmxs
 ./test/test.v
diff --git a/test-suite/coq-makefile/multiroot/run.sh b/test-suite/coq-makefile/multiroot/run.sh
index 863c39f50..3cd1ac305 100755
--- a/test-suite/coq-makefile/multiroot/run.sh
+++ b/test-suite/coq-makefile/multiroot/run.sh
@@ -19,12 +19,9 @@ sort > desired <<EOT
 ./test
 ./test/test.glob
 ./test/test.cmi
-./test/test.cmo
 ./test/test.cmx
 ./test/test_aux.cmi
-./test/test_aux.cmo
 ./test/test_aux.cmx
-./test/test_plugin.cma
 ./test/test_plugin.cmxa
 ./test/test_plugin.cmxs
 ./test/test.v
diff --git a/test-suite/coq-makefile/native1/run.sh b/test-suite/coq-makefile/native1/run.sh
index f07966263..9f6295d64 100755
--- a/test-suite/coq-makefile/native1/run.sh
+++ b/test-suite/coq-makefile/native1/run.sh
@@ -18,9 +18,7 @@ sort > desired <<EOT
 .
 ./test
 ./test/test.glob
-./test/test_plugin.cma
 ./test/test_plugin.cmi
-./test/test_plugin.cmo
 ./test/test_plugin.cmx
 ./test/test_plugin.cmxs
 ./test/test.v
diff --git a/test-suite/coq-makefile/plugin-reach-outside-API-and-fail/run.sh b/test-suite/coq-makefile/plugin-reach-outside-API-and-fail/run.sh
new file mode 100755
index 000000000..6301aa03c
--- /dev/null
+++ b/test-suite/coq-makefile/plugin-reach-outside-API-and-fail/run.sh
@@ -0,0 +1,37 @@
+#!/usr/bin/env bash
+
+set -e
+
+git clean -dfx
+
+cat > _CoqProject <<EOT
+-I src/
+
+./src/test_plugin.mllib
+./src/test.ml4
+./src/test.mli
+EOT
+
+mkdir src
+
+cat > src/test_plugin.mllib <<EOT
+Test
+EOT
+
+touch src/test.mli
+
+cat > src/test.ml4 <<EOT
+DECLARE PLUGIN "test"
+
+let _ = Pre_env.empty_env
+EOT
+
+${COQBIN}coq_makefile -f _CoqProject -o Makefile
+
+if make VERBOSE=1; then
+  # make command should have failed (but didn't)
+  exit 1
+else
+  # make command should have failed (and it indeed did)
+  exit 0
+fi
diff --git a/test-suite/coq-makefile/plugin-reach-outside-API-and-succeed-by-bypassing-the-API/run.sh b/test-suite/coq-makefile/plugin-reach-outside-API-and-succeed-by-bypassing-the-API/run.sh
new file mode 100755
index 000000000..991fb4a61
--- /dev/null
+++ b/test-suite/coq-makefile/plugin-reach-outside-API-and-succeed-by-bypassing-the-API/run.sh
@@ -0,0 +1,32 @@
+#!/usr/bin/env bash
+
+set -e
+
+git clean -dfx
+
+cat > _CoqProject <<EOT
+-bypass-API
+-I src/
+
+./src/test_plugin.mllib
+./src/test.ml4
+./src/test.mli
+EOT
+
+mkdir src
+
+cat > src/test_plugin.mllib <<EOT
+Test
+EOT
+
+touch src/test.mli
+
+cat > src/test.ml4 <<EOT
+DECLARE PLUGIN "test"
+
+let _ = Pre_env.empty_env
+EOT
+
+${COQBIN}coq_makefile -f _CoqProject -o Makefile
+
+make VERBOSE=1
diff --git a/test-suite/coq-makefile/plugin1/run.sh b/test-suite/coq-makefile/plugin1/run.sh
index 24ef8c891..c2d47166f 100755
--- a/test-suite/coq-makefile/plugin1/run.sh
+++ b/test-suite/coq-makefile/plugin1/run.sh
@@ -17,12 +17,9 @@ sort > desired <<EOT
 ./test
 ./test/test.glob
 ./test/test.cmi
-./test/test.cmo
 ./test/test.cmx
 ./test/test_aux.cmi
-./test/test_aux.cmo
 ./test/test_aux.cmx
-./test/test_plugin.cma
 ./test/test_plugin.cmxa
 ./test/test_plugin.cmxs
 ./test/test.v
diff --git a/test-suite/coq-makefile/plugin2/run.sh b/test-suite/coq-makefile/plugin2/run.sh
index 24ef8c891..c2d47166f 100755
--- a/test-suite/coq-makefile/plugin2/run.sh
+++ b/test-suite/coq-makefile/plugin2/run.sh
@@ -17,12 +17,9 @@ sort > desired <<EOT
 ./test
 ./test/test.glob
 ./test/test.cmi
-./test/test.cmo
 ./test/test.cmx
 ./test/test_aux.cmi
-./test/test_aux.cmo
 ./test/test_aux.cmx
-./test/test_plugin.cma
 ./test/test_plugin.cmxa
 ./test/test_plugin.cmxs
 ./test/test.v
diff --git a/test-suite/coq-makefile/plugin3/run.sh b/test-suite/coq-makefile/plugin3/run.sh
index 24ef8c891..c2d47166f 100755
--- a/test-suite/coq-makefile/plugin3/run.sh
+++ b/test-suite/coq-makefile/plugin3/run.sh
@@ -17,12 +17,9 @@ sort > desired <<EOT
 ./test
 ./test/test.glob
 ./test/test.cmi
-./test/test.cmo
 ./test/test.cmx
 ./test/test_aux.cmi
-./test/test_aux.cmo
 ./test/test_aux.cmx
-./test/test_plugin.cma
 ./test/test_plugin.cmxa
 ./test/test_plugin.cmxs
 ./test/test.v
diff --git a/test-suite/coq-makefile/template/src/test.ml4 b/test-suite/coq-makefile/template/src/test.ml4
index 72765abe0..e7d0bfe1f 100644
--- a/test-suite/coq-makefile/template/src/test.ml4
+++ b/test-suite/coq-makefile/template/src/test.ml4
@@ -1,3 +1,4 @@
+open API
 open Ltac_plugin
 DECLARE PLUGIN "test_plugin"
 let () = Mltop.add_known_plugin (fun () -> ()) "test_plugin";;
diff --git a/test-suite/coq-makefile/template/src/test_aux.ml b/test-suite/coq-makefile/template/src/test_aux.ml
index a01d0865a..e134abd84 100644
--- a/test-suite/coq-makefile/template/src/test_aux.ml
+++ b/test-suite/coq-makefile/template/src/test_aux.ml
@@ -1 +1 @@
-let tac = Proofview.tclUNIT ()
+let tac = API.Proofview.tclUNIT ()
diff --git a/test-suite/coq-makefile/template/src/test_aux.mli b/test-suite/coq-makefile/template/src/test_aux.mli
index 10020f27d..2e7ad1529 100644
--- a/test-suite/coq-makefile/template/src/test_aux.mli
+++ b/test-suite/coq-makefile/template/src/test_aux.mli
@@ -1 +1 @@
-val tac : unit Proofview.tactic
+val tac : unit API.Proofview.tactic
diff --git a/test-suite/save-logs.sh b/test-suite/save-logs.sh
index fb8a1c1b0..b61362108 100755
--- a/test-suite/save-logs.sh
+++ b/test-suite/save-logs.sh
@@ -9,7 +9,7 @@ mkdir "$SAVEDIR"
 # keep this synced with test-suite/Makefile
 FAILMARK="==========> FAILURE <=========="
 
-FAILED=$(mktemp)
+FAILED=$(mktemp /tmp/coq-check-XXXXX)
 find . '(' -path ./bugs/opened -prune ')' -o '(' -name '*.log' -exec grep "$FAILMARK" -q '{}' ';' -print0 ')' > "$FAILED"
 
 rsync -a --from0 --files-from="$FAILED" . "$SAVEDIR"