From 352c23666babc7dd8f0136b02d9ef1893f9bde5c Mon Sep 17 00:00:00 2001
From: Enrico Tassi <Enrico.Tassi@inria.fr>
Date: Mon, 23 Jan 2017 17:32:58 +0100
Subject: test suite for coq_makefile2

---
 .gitignore                                         |  3 +-
 test-suite/Makefile                                |  2 +-
 test-suite/coq-makefile/compat-subdirs/_CoqProject |  4 +-
 test-suite/coq-makefile/compat-subdirs/run.sh      |  3 +-
 .../coq-makefile/compat-subdirs/src/test.ml4       | 13 -----
 .../coq-makefile/compat-subdirs/src/test.mli       |  0
 .../coq-makefile/compat-subdirs/src/test_aux.ml    |  1 -
 .../coq-makefile/compat-subdirs/src/test_aux.mli   |  1 -
 .../compat-subdirs/src/test_plugin.mlpack          |  2 -
 .../coq-makefile/compat-subdirs/theories/test.v    |  7 ---
 test-suite/coq-makefile/coqdoc1/run.sh             |  4 +-
 test-suite/coq-makefile/coqdoc1/src/test.ml4       | 13 -----
 test-suite/coq-makefile/coqdoc1/src/test.mli       |  0
 test-suite/coq-makefile/coqdoc1/src/test_aux.ml    |  1 -
 test-suite/coq-makefile/coqdoc1/src/test_aux.mli   |  1 -
 .../coq-makefile/coqdoc1/src/test_plugin.mlpack    |  2 -
 .../coq-makefile/coqdoc1/theories/sub/testsub.v    |  1 -
 test-suite/coq-makefile/coqdoc1/theories/test.v    |  7 ---
 test-suite/coq-makefile/coqdoc2/_CoqProject        | 11 ++++
 test-suite/coq-makefile/coqdoc2/run.sh             | 53 +++++++++++++++++++
 .../coq-makefile/extend-subdirs/Makefile.local     |  4 ++
 test-suite/coq-makefile/extend-subdirs/_CoqProject | 10 ++++
 test-suite/coq-makefile/extend-subdirs/run.sh      | 10 ++++
 .../coq-makefile/extend-subdirs/subdir/Makefile    |  5 ++
 test-suite/coq-makefile/latex1/_CoqProject         | 11 ++++
 test-suite/coq-makefile/latex1/run.sh              | 15 ++++++
 test-suite/coq-makefile/merlin1/_CoqProject        |  4 +-
 test-suite/coq-makefile/merlin1/run.sh             | 10 ++--
 test-suite/coq-makefile/merlin1/src/test.ml4       | 13 -----
 test-suite/coq-makefile/merlin1/src/test.mli       |  0
 test-suite/coq-makefile/merlin1/src/test_aux.ml    |  1 -
 test-suite/coq-makefile/merlin1/src/test_aux.mli   |  1 -
 .../coq-makefile/merlin1/src/test_plugin.mlpack    |  2 -
 test-suite/coq-makefile/merlin1/theories/test.v    |  7 ---
 test-suite/coq-makefile/mllib1/_CoqProject         |  9 ----
 test-suite/coq-makefile/mllib1/run.sh              | 30 -----------
 test-suite/coq-makefile/mllib1/src/test.ml4        | 13 -----
 test-suite/coq-makefile/mllib1/src/test.mli        |  0
 test-suite/coq-makefile/mllib1/src/test_aux.ml     |  1 -
 test-suite/coq-makefile/mllib1/src/test_aux.mli    |  1 -
 .../coq-makefile/mllib1/src/test_plugin.mllib      |  2 -
 test-suite/coq-makefile/mllib1/theories/test.v     |  7 ---
 test-suite/coq-makefile/mlpack1/_CoqProject        |  4 +-
 test-suite/coq-makefile/mlpack1/run.sh             |  4 +-
 test-suite/coq-makefile/mlpack1/src/test.ml4       | 13 -----
 test-suite/coq-makefile/mlpack1/src/test.mli       |  0
 test-suite/coq-makefile/mlpack1/src/test_aux.ml    |  1 -
 test-suite/coq-makefile/mlpack1/src/test_aux.mli   |  1 -
 .../coq-makefile/mlpack1/src/test_plugin.mlpack    |  2 -
 test-suite/coq-makefile/mlpack1/theories/test.v    |  7 ---
 test-suite/coq-makefile/mlpack2/_CoqProject        | 10 ++++
 test-suite/coq-makefile/mlpack2/run.sh             | 25 +++++++++
 test-suite/coq-makefile/multiroot/_CoqProject      | 12 +++++
 test-suite/coq-makefile/multiroot/run.sh           | 61 ++++++++++++++++++++++
 test-suite/coq-makefile/native1/_CoqProject        | 11 ++++
 test-suite/coq-makefile/native1/run.sh             | 34 ++++++++++++
 test-suite/coq-makefile/plugin1/_CoqProject        | 10 ++++
 test-suite/coq-makefile/plugin1/run.sh             | 31 +++++++++++
 test-suite/coq-makefile/plugin2/_CoqProject        | 10 ++++
 test-suite/coq-makefile/plugin2/run.sh             | 31 +++++++++++
 test-suite/coq-makefile/plugin3/_CoqProject        | 10 ++++
 test-suite/coq-makefile/plugin3/run.sh             | 31 +++++++++++
 test-suite/coq-makefile/template/init.sh           | 16 ++++++
 test-suite/coq-makefile/template/src/test.ml4      | 14 +++++
 test-suite/coq-makefile/template/src/test.mli      |  0
 test-suite/coq-makefile/template/src/test_aux.ml   |  1 +
 test-suite/coq-makefile/template/src/test_aux.mli  |  1 +
 .../coq-makefile/template/src/test_plugin.mlpack   |  2 +
 .../coq-makefile/template/theories/sub/testsub.v   |  1 +
 test-suite/coq-makefile/template/theories/test.v   |  7 +++
 test-suite/coq-makefile/uninstall1/_CoqProject     |  4 +-
 test-suite/coq-makefile/uninstall1/run.sh          |  4 +-
 test-suite/coq-makefile/uninstall1/src/test.ml4    | 13 -----
 test-suite/coq-makefile/uninstall1/src/test.mli    |  0
 test-suite/coq-makefile/uninstall1/src/test_aux.ml |  1 -
 .../coq-makefile/uninstall1/src/test_aux.mli       |  1 -
 .../coq-makefile/uninstall1/src/test_plugin.mlpack |  2 -
 .../coq-makefile/uninstall1/theories/sub/testsub.v |  1 -
 test-suite/coq-makefile/uninstall1/theories/test.v |  7 ---
 test-suite/coq-makefile/uninstall2/_CoqProject     | 11 ++++
 test-suite/coq-makefile/uninstall2/run.sh          | 20 +++++++
 test-suite/coq-makefile/validate1/_CoqProject      | 10 ++++
 test-suite/coq-makefile/validate1/run.sh           | 10 ++++
 83 files changed, 512 insertions(+), 207 deletions(-)
 delete mode 100644 test-suite/coq-makefile/compat-subdirs/src/test.ml4
 delete mode 100644 test-suite/coq-makefile/compat-subdirs/src/test.mli
 delete mode 100644 test-suite/coq-makefile/compat-subdirs/src/test_aux.ml
 delete mode 100644 test-suite/coq-makefile/compat-subdirs/src/test_aux.mli
 delete mode 100644 test-suite/coq-makefile/compat-subdirs/src/test_plugin.mlpack
 delete mode 100644 test-suite/coq-makefile/compat-subdirs/theories/test.v
 delete mode 100644 test-suite/coq-makefile/coqdoc1/src/test.ml4
 delete mode 100644 test-suite/coq-makefile/coqdoc1/src/test.mli
 delete mode 100644 test-suite/coq-makefile/coqdoc1/src/test_aux.ml
 delete mode 100644 test-suite/coq-makefile/coqdoc1/src/test_aux.mli
 delete mode 100644 test-suite/coq-makefile/coqdoc1/src/test_plugin.mlpack
 delete mode 100644 test-suite/coq-makefile/coqdoc1/theories/sub/testsub.v
 delete mode 100644 test-suite/coq-makefile/coqdoc1/theories/test.v
 create mode 100644 test-suite/coq-makefile/coqdoc2/_CoqProject
 create mode 100755 test-suite/coq-makefile/coqdoc2/run.sh
 create mode 100644 test-suite/coq-makefile/extend-subdirs/Makefile.local
 create mode 100644 test-suite/coq-makefile/extend-subdirs/_CoqProject
 create mode 100755 test-suite/coq-makefile/extend-subdirs/run.sh
 create mode 100644 test-suite/coq-makefile/extend-subdirs/subdir/Makefile
 create mode 100644 test-suite/coq-makefile/latex1/_CoqProject
 create mode 100755 test-suite/coq-makefile/latex1/run.sh
 delete mode 100644 test-suite/coq-makefile/merlin1/src/test.ml4
 delete mode 100644 test-suite/coq-makefile/merlin1/src/test.mli
 delete mode 100644 test-suite/coq-makefile/merlin1/src/test_aux.ml
 delete mode 100644 test-suite/coq-makefile/merlin1/src/test_aux.mli
 delete mode 100644 test-suite/coq-makefile/merlin1/src/test_plugin.mlpack
 delete mode 100644 test-suite/coq-makefile/merlin1/theories/test.v
 delete mode 100644 test-suite/coq-makefile/mllib1/_CoqProject
 delete mode 100755 test-suite/coq-makefile/mllib1/run.sh
 delete mode 100644 test-suite/coq-makefile/mllib1/src/test.ml4
 delete mode 100644 test-suite/coq-makefile/mllib1/src/test.mli
 delete mode 100644 test-suite/coq-makefile/mllib1/src/test_aux.ml
 delete mode 100644 test-suite/coq-makefile/mllib1/src/test_aux.mli
 delete mode 100644 test-suite/coq-makefile/mllib1/src/test_plugin.mllib
 delete mode 100644 test-suite/coq-makefile/mllib1/theories/test.v
 delete mode 100644 test-suite/coq-makefile/mlpack1/src/test.ml4
 delete mode 100644 test-suite/coq-makefile/mlpack1/src/test.mli
 delete mode 100644 test-suite/coq-makefile/mlpack1/src/test_aux.ml
 delete mode 100644 test-suite/coq-makefile/mlpack1/src/test_aux.mli
 delete mode 100644 test-suite/coq-makefile/mlpack1/src/test_plugin.mlpack
 delete mode 100644 test-suite/coq-makefile/mlpack1/theories/test.v
 create mode 100644 test-suite/coq-makefile/mlpack2/_CoqProject
 create mode 100755 test-suite/coq-makefile/mlpack2/run.sh
 create mode 100644 test-suite/coq-makefile/multiroot/_CoqProject
 create mode 100755 test-suite/coq-makefile/multiroot/run.sh
 create mode 100644 test-suite/coq-makefile/native1/_CoqProject
 create mode 100755 test-suite/coq-makefile/native1/run.sh
 create mode 100644 test-suite/coq-makefile/plugin1/_CoqProject
 create mode 100755 test-suite/coq-makefile/plugin1/run.sh
 create mode 100644 test-suite/coq-makefile/plugin2/_CoqProject
 create mode 100755 test-suite/coq-makefile/plugin2/run.sh
 create mode 100644 test-suite/coq-makefile/plugin3/_CoqProject
 create mode 100755 test-suite/coq-makefile/plugin3/run.sh
 create mode 100644 test-suite/coq-makefile/template/init.sh
 create mode 100644 test-suite/coq-makefile/template/src/test.ml4
 create mode 100644 test-suite/coq-makefile/template/src/test.mli
 create mode 100644 test-suite/coq-makefile/template/src/test_aux.ml
 create mode 100644 test-suite/coq-makefile/template/src/test_aux.mli
 create mode 100644 test-suite/coq-makefile/template/src/test_plugin.mlpack
 create mode 100644 test-suite/coq-makefile/template/theories/sub/testsub.v
 create mode 100644 test-suite/coq-makefile/template/theories/test.v
 delete mode 100644 test-suite/coq-makefile/uninstall1/src/test.ml4
 delete mode 100644 test-suite/coq-makefile/uninstall1/src/test.mli
 delete mode 100644 test-suite/coq-makefile/uninstall1/src/test_aux.ml
 delete mode 100644 test-suite/coq-makefile/uninstall1/src/test_aux.mli
 delete mode 100644 test-suite/coq-makefile/uninstall1/src/test_plugin.mlpack
 delete mode 100644 test-suite/coq-makefile/uninstall1/theories/sub/testsub.v
 delete mode 100644 test-suite/coq-makefile/uninstall1/theories/test.v
 create mode 100644 test-suite/coq-makefile/uninstall2/_CoqProject
 create mode 100755 test-suite/coq-makefile/uninstall2/run.sh
 create mode 100644 test-suite/coq-makefile/validate1/_CoqProject
 create mode 100755 test-suite/coq-makefile/validate1/run.sh

diff --git a/.gitignore b/.gitignore
index 6e6f01a43..c55ad24f8 100644
--- a/.gitignore
+++ b/.gitignore
@@ -64,7 +64,8 @@ test-suite/coq-makefile/*/actual
 test-suite/coq-makefile/*/desired
 test-suite/coq-makefile/*/Makefile
 test-suite/coq-makefile/*/Makefile.conf
-test-suite/coq-makefile/*/src/test.ml
+test-suite/coq-makefile/*/src
+test-suite/coq-makefile/*/theories
 test-suite/coq-makefile/*/html
 test-suite/coq-makefile/*/mlihtml
 test-suite/coq-makefile/*/subdir/done
diff --git a/test-suite/Makefile b/test-suite/Makefile
index 8a3d383cb..c2d6e540c 100644
--- a/test-suite/Makefile
+++ b/test-suite/Makefile
@@ -486,7 +486,7 @@ coqchk: $(patsubst %.v,%.chk.log,$(wildcard coqchk/*.v))
 coq-makefile: $(patsubst %/run.sh,%.log,$(wildcard coq-makefile/*/run.sh))
 
 coq-makefile/%.log : coq-makefile/%/run.sh
-	@echo "TEST      $*"
+	@echo "TEST      coq-makefile/$*"
 	$(HIDE)(\
 	  cd coq-makefile/$* && \
 	  ./run.sh 2>&1; \
diff --git a/test-suite/coq-makefile/compat-subdirs/_CoqProject b/test-suite/coq-makefile/compat-subdirs/_CoqProject
index 700d59d64..4f44bde22 100644
--- a/test-suite/coq-makefile/compat-subdirs/_CoqProject
+++ b/test-suite/coq-makefile/compat-subdirs/_CoqProject
@@ -1,5 +1,5 @@
--R src/ test
--R theories/ test
+-R src test
+-R theories test
 -I src
 
 src/test_plugin.mlpack
diff --git a/test-suite/coq-makefile/compat-subdirs/run.sh b/test-suite/coq-makefile/compat-subdirs/run.sh
index 38e54d03e..ccb348c6f 100755
--- a/test-suite/coq-makefile/compat-subdirs/run.sh
+++ b/test-suite/coq-makefile/compat-subdirs/run.sh
@@ -3,8 +3,7 @@
 #set -x
 set -e
 
-export PATH=../../../bin/:$PATH
-git clean -dfx .
+. ../template/init.sh
 coq_makefile -f _CoqProject -o Makefile
 make
 exec test -f "subdir/done"
diff --git a/test-suite/coq-makefile/compat-subdirs/src/test.ml4 b/test-suite/coq-makefile/compat-subdirs/src/test.ml4
deleted file mode 100644
index 8ddc9b095..000000000
--- a/test-suite/coq-makefile/compat-subdirs/src/test.ml4
+++ /dev/null
@@ -1,13 +0,0 @@
-DECLARE PLUGIN "test_plugin"
-let () = Mltop.add_known_plugin (fun () -> ()) "test_plugin";;
-
-VERNAC COMMAND EXTEND Test CLASSIFIED AS SIDEFF
-  | [ "Test" ] -> [ () ]
-END
-
-TACTIC EXTEND test
-| [ "test" ] -> [ Test_aux.tac ]
-END
-
-
-
diff --git a/test-suite/coq-makefile/compat-subdirs/src/test.mli b/test-suite/coq-makefile/compat-subdirs/src/test.mli
deleted file mode 100644
index e69de29bb..000000000
diff --git a/test-suite/coq-makefile/compat-subdirs/src/test_aux.ml b/test-suite/coq-makefile/compat-subdirs/src/test_aux.ml
deleted file mode 100644
index a01d0865a..000000000
--- a/test-suite/coq-makefile/compat-subdirs/src/test_aux.ml
+++ /dev/null
@@ -1 +0,0 @@
-let tac = Proofview.tclUNIT ()
diff --git a/test-suite/coq-makefile/compat-subdirs/src/test_aux.mli b/test-suite/coq-makefile/compat-subdirs/src/test_aux.mli
deleted file mode 100644
index 10020f27d..000000000
--- a/test-suite/coq-makefile/compat-subdirs/src/test_aux.mli
+++ /dev/null
@@ -1 +0,0 @@
-val tac : unit Proofview.tactic
diff --git a/test-suite/coq-makefile/compat-subdirs/src/test_plugin.mlpack b/test-suite/coq-makefile/compat-subdirs/src/test_plugin.mlpack
deleted file mode 100644
index cf94d851b..000000000
--- a/test-suite/coq-makefile/compat-subdirs/src/test_plugin.mlpack
+++ /dev/null
@@ -1,2 +0,0 @@
-Test_aux
-Test
diff --git a/test-suite/coq-makefile/compat-subdirs/theories/test.v b/test-suite/coq-makefile/compat-subdirs/theories/test.v
deleted file mode 100644
index 7753b56aa..000000000
--- a/test-suite/coq-makefile/compat-subdirs/theories/test.v
+++ /dev/null
@@ -1,7 +0,0 @@
-Declare ML Module "test_plugin".
-Test.
-Goal True.
-Proof.
-test.
-exact I.
-Qed.
diff --git a/test-suite/coq-makefile/coqdoc1/run.sh b/test-suite/coq-makefile/coqdoc1/run.sh
index bbe9717ab..e071f1db7 100755
--- a/test-suite/coq-makefile/coqdoc1/run.sh
+++ b/test-suite/coq-makefile/coqdoc1/run.sh
@@ -3,8 +3,8 @@
 #set -x
 set -e
 
-export PATH=../../../bin/:$PATH
-git clean -dfx .
+. ../template/init.sh
+
 coq_makefile -f _CoqProject -o Makefile
 make
 make html mlihtml
diff --git a/test-suite/coq-makefile/coqdoc1/src/test.ml4 b/test-suite/coq-makefile/coqdoc1/src/test.ml4
deleted file mode 100644
index 8ddc9b095..000000000
--- a/test-suite/coq-makefile/coqdoc1/src/test.ml4
+++ /dev/null
@@ -1,13 +0,0 @@
-DECLARE PLUGIN "test_plugin"
-let () = Mltop.add_known_plugin (fun () -> ()) "test_plugin";;
-
-VERNAC COMMAND EXTEND Test CLASSIFIED AS SIDEFF
-  | [ "Test" ] -> [ () ]
-END
-
-TACTIC EXTEND test
-| [ "test" ] -> [ Test_aux.tac ]
-END
-
-
-
diff --git a/test-suite/coq-makefile/coqdoc1/src/test.mli b/test-suite/coq-makefile/coqdoc1/src/test.mli
deleted file mode 100644
index e69de29bb..000000000
diff --git a/test-suite/coq-makefile/coqdoc1/src/test_aux.ml b/test-suite/coq-makefile/coqdoc1/src/test_aux.ml
deleted file mode 100644
index a01d0865a..000000000
--- a/test-suite/coq-makefile/coqdoc1/src/test_aux.ml
+++ /dev/null
@@ -1 +0,0 @@
-let tac = Proofview.tclUNIT ()
diff --git a/test-suite/coq-makefile/coqdoc1/src/test_aux.mli b/test-suite/coq-makefile/coqdoc1/src/test_aux.mli
deleted file mode 100644
index 10020f27d..000000000
--- a/test-suite/coq-makefile/coqdoc1/src/test_aux.mli
+++ /dev/null
@@ -1 +0,0 @@
-val tac : unit Proofview.tactic
diff --git a/test-suite/coq-makefile/coqdoc1/src/test_plugin.mlpack b/test-suite/coq-makefile/coqdoc1/src/test_plugin.mlpack
deleted file mode 100644
index cf94d851b..000000000
--- a/test-suite/coq-makefile/coqdoc1/src/test_plugin.mlpack
+++ /dev/null
@@ -1,2 +0,0 @@
-Test_aux
-Test
diff --git a/test-suite/coq-makefile/coqdoc1/theories/sub/testsub.v b/test-suite/coq-makefile/coqdoc1/theories/sub/testsub.v
deleted file mode 100644
index 755fc343f..000000000
--- a/test-suite/coq-makefile/coqdoc1/theories/sub/testsub.v
+++ /dev/null
@@ -1 +0,0 @@
-Require Import test.
diff --git a/test-suite/coq-makefile/coqdoc1/theories/test.v b/test-suite/coq-makefile/coqdoc1/theories/test.v
deleted file mode 100644
index 7753b56aa..000000000
--- a/test-suite/coq-makefile/coqdoc1/theories/test.v
+++ /dev/null
@@ -1,7 +0,0 @@
-Declare ML Module "test_plugin".
-Test.
-Goal True.
-Proof.
-test.
-exact I.
-Qed.
diff --git a/test-suite/coq-makefile/coqdoc2/_CoqProject b/test-suite/coq-makefile/coqdoc2/_CoqProject
new file mode 100644
index 000000000..d2a547d47
--- /dev/null
+++ b/test-suite/coq-makefile/coqdoc2/_CoqProject
@@ -0,0 +1,11 @@
+-R src/ test
+-R theories/ test
+-I src/
+
+src/test_plugin.mlpack
+src/test.ml4
+src/test.mli
+src/test_aux.ml
+src/test_aux.mli
+theories/test.v
+theories/sub/testsub.v
diff --git a/test-suite/coq-makefile/coqdoc2/run.sh b/test-suite/coq-makefile/coqdoc2/run.sh
new file mode 100755
index 000000000..e071f1db7
--- /dev/null
+++ b/test-suite/coq-makefile/coqdoc2/run.sh
@@ -0,0 +1,53 @@
+#!/bin/bash
+
+#set -x
+set -e
+
+. ../template/init.sh
+
+coq_makefile -f _CoqProject -o Makefile
+make
+make html mlihtml
+make install DSTROOT="$PWD/tmp"
+make install-doc DSTROOT="$PWD/tmp"
+#make debug
+(for d in `find tmp -name user-contrib`; do pushd $d >/dev/null; find; popd >/dev/null; done) | sort -u > actual
+sort -u > desired <<EOT
+.
+./test
+./test/test_plugin.cmi
+./test/test_plugin.cmo
+./test/test_plugin.cmx
+./test/test_plugin.cmxs
+./test/test.glob
+./test/test.v
+./test/test.vo
+./test/sub
+./test/sub/testsub.glob
+./test/sub/testsub.v
+./test/sub/testsub.vo
+./test/mlihtml
+./test/mlihtml/index_exceptions.html
+./test/mlihtml/index.html
+./test/mlihtml/index_class_types.html
+./test/mlihtml/type_Test_aux.html
+./test/mlihtml/index_module_types.html
+./test/mlihtml/index_classes.html
+./test/mlihtml/type_Test.html
+./test/mlihtml/style.css
+./test/mlihtml/index_attributes.html
+./test/mlihtml/index_types.html
+./test/mlihtml/Test_aux.html
+./test/mlihtml/index_values.html
+./test/mlihtml/Test.html
+./test/mlihtml/index_extensions.html
+./test/mlihtml/index_methods.html
+./test/mlihtml/index_modules.html
+./test/html
+./test/html/index.html
+./test/html/test.sub.testsub.html
+./test/html/toc.html
+./test/html/coqdoc.css
+./test/html/test.test.html
+EOT
+exec diff -u desired actual
diff --git a/test-suite/coq-makefile/extend-subdirs/Makefile.local b/test-suite/coq-makefile/extend-subdirs/Makefile.local
new file mode 100644
index 000000000..b031d30db
--- /dev/null
+++ b/test-suite/coq-makefile/extend-subdirs/Makefile.local
@@ -0,0 +1,4 @@
+pre-all::
+	$(MAKE) -C subdir pre
+post-all::
+	$(MAKE) -C subdir post
diff --git a/test-suite/coq-makefile/extend-subdirs/_CoqProject b/test-suite/coq-makefile/extend-subdirs/_CoqProject
new file mode 100644
index 000000000..69f47302e
--- /dev/null
+++ b/test-suite/coq-makefile/extend-subdirs/_CoqProject
@@ -0,0 +1,10 @@
+-R src test
+-R theories test
+-I src
+
+src/test_plugin.mlpack
+src/test.ml4
+src/test.mli
+src/test_aux.ml
+src/test_aux.mli
+theories/test.v
diff --git a/test-suite/coq-makefile/extend-subdirs/run.sh b/test-suite/coq-makefile/extend-subdirs/run.sh
new file mode 100755
index 000000000..db1160113
--- /dev/null
+++ b/test-suite/coq-makefile/extend-subdirs/run.sh
@@ -0,0 +1,10 @@
+#!/bin/sh
+
+#set -x
+set -e
+
+. ../template/init.sh
+
+coq_makefile -f _CoqProject -o Makefile
+make
+exec test -f "subdir/done"
diff --git a/test-suite/coq-makefile/extend-subdirs/subdir/Makefile b/test-suite/coq-makefile/extend-subdirs/subdir/Makefile
new file mode 100644
index 000000000..23f52b154
--- /dev/null
+++ b/test-suite/coq-makefile/extend-subdirs/subdir/Makefile
@@ -0,0 +1,5 @@
+pre:
+	test ! -f ../theories/test.vo
+post:
+	test -f ../theories/test.vo
+	touch done
diff --git a/test-suite/coq-makefile/latex1/_CoqProject b/test-suite/coq-makefile/latex1/_CoqProject
new file mode 100644
index 000000000..35792066b
--- /dev/null
+++ b/test-suite/coq-makefile/latex1/_CoqProject
@@ -0,0 +1,11 @@
+-R src test
+-R theories test
+-I src
+
+src/test_plugin.mlpack
+src/test.ml4
+src/test.mli
+src/test_aux.ml
+src/test_aux.mli
+theories/test.v
+theories/sub/testsub.v
diff --git a/test-suite/coq-makefile/latex1/run.sh b/test-suite/coq-makefile/latex1/run.sh
new file mode 100755
index 000000000..45f226911
--- /dev/null
+++ b/test-suite/coq-makefile/latex1/run.sh
@@ -0,0 +1,15 @@
+#!/bin/bash
+
+#set -x
+set -e
+
+if which pdflatex; then
+
+. ../template/init.sh
+	
+coq_makefile -f _CoqProject -o Makefile
+make
+exec make all.pdf
+
+fi
+exit 0 # test skipped
diff --git a/test-suite/coq-makefile/merlin1/_CoqProject b/test-suite/coq-makefile/merlin1/_CoqProject
index cb1ad4a4b..69f47302e 100644
--- a/test-suite/coq-makefile/merlin1/_CoqProject
+++ b/test-suite/coq-makefile/merlin1/_CoqProject
@@ -1,5 +1,5 @@
--R src/ test
--R theories/ test
+-R src test
+-R theories test
 -I src
 
 src/test_plugin.mlpack
diff --git a/test-suite/coq-makefile/merlin1/run.sh b/test-suite/coq-makefile/merlin1/run.sh
index 3b5d388c9..9b89e5b6e 100755
--- a/test-suite/coq-makefile/merlin1/run.sh
+++ b/test-suite/coq-makefile/merlin1/run.sh
@@ -3,11 +3,13 @@
 #set -x
 set -e
 
-export PATH=../../../bin/:$PATH
-git clean -dfx .
+. ../template/init.sh
+
 coq_makefile -f _CoqProject -o Makefile
 make .merlin
-echo B $PWD/src > desired
-echo S $PWD/src >> desired
+cat > desired <<EOT
+B src
+S src
+EOT
 tail -2 .merlin > actual
 exec diff -u desired actual
diff --git a/test-suite/coq-makefile/merlin1/src/test.ml4 b/test-suite/coq-makefile/merlin1/src/test.ml4
deleted file mode 100644
index 8ddc9b095..000000000
--- a/test-suite/coq-makefile/merlin1/src/test.ml4
+++ /dev/null
@@ -1,13 +0,0 @@
-DECLARE PLUGIN "test_plugin"
-let () = Mltop.add_known_plugin (fun () -> ()) "test_plugin";;
-
-VERNAC COMMAND EXTEND Test CLASSIFIED AS SIDEFF
-  | [ "Test" ] -> [ () ]
-END
-
-TACTIC EXTEND test
-| [ "test" ] -> [ Test_aux.tac ]
-END
-
-
-
diff --git a/test-suite/coq-makefile/merlin1/src/test.mli b/test-suite/coq-makefile/merlin1/src/test.mli
deleted file mode 100644
index e69de29bb..000000000
diff --git a/test-suite/coq-makefile/merlin1/src/test_aux.ml b/test-suite/coq-makefile/merlin1/src/test_aux.ml
deleted file mode 100644
index a01d0865a..000000000
--- a/test-suite/coq-makefile/merlin1/src/test_aux.ml
+++ /dev/null
@@ -1 +0,0 @@
-let tac = Proofview.tclUNIT ()
diff --git a/test-suite/coq-makefile/merlin1/src/test_aux.mli b/test-suite/coq-makefile/merlin1/src/test_aux.mli
deleted file mode 100644
index 10020f27d..000000000
--- a/test-suite/coq-makefile/merlin1/src/test_aux.mli
+++ /dev/null
@@ -1 +0,0 @@
-val tac : unit Proofview.tactic
diff --git a/test-suite/coq-makefile/merlin1/src/test_plugin.mlpack b/test-suite/coq-makefile/merlin1/src/test_plugin.mlpack
deleted file mode 100644
index cf94d851b..000000000
--- a/test-suite/coq-makefile/merlin1/src/test_plugin.mlpack
+++ /dev/null
@@ -1,2 +0,0 @@
-Test_aux
-Test
diff --git a/test-suite/coq-makefile/merlin1/theories/test.v b/test-suite/coq-makefile/merlin1/theories/test.v
deleted file mode 100644
index 7753b56aa..000000000
--- a/test-suite/coq-makefile/merlin1/theories/test.v
+++ /dev/null
@@ -1,7 +0,0 @@
-Declare ML Module "test_plugin".
-Test.
-Goal True.
-Proof.
-test.
-exact I.
-Qed.
diff --git a/test-suite/coq-makefile/mllib1/_CoqProject b/test-suite/coq-makefile/mllib1/_CoqProject
deleted file mode 100644
index 6b2046d68..000000000
--- a/test-suite/coq-makefile/mllib1/_CoqProject
+++ /dev/null
@@ -1,9 +0,0 @@
--R theories test
--I src
-
-src/test_plugin.mllib
-src/test.ml4
-src/test.mli
-src/test_aux.ml
-src/test_aux.mli
-theories/test.v
diff --git a/test-suite/coq-makefile/mllib1/run.sh b/test-suite/coq-makefile/mllib1/run.sh
deleted file mode 100755
index 8f6b8e7ea..000000000
--- a/test-suite/coq-makefile/mllib1/run.sh
+++ /dev/null
@@ -1,30 +0,0 @@
-#!/bin/sh
-
-#set -x
-set -e
-
-export PATH=../../../bin/:$PATH
-git clean -dfx .
-coq_makefile -f _CoqProject -o Makefile
-make
-make html mlihtml
-make install DSTROOT="$PWD/tmp"
-#make debug
-(cd `find tmp -name user-contrib`; find) | sort > actual
-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
-./test/test.vo
-EOT
-exec diff -u desired actual
diff --git a/test-suite/coq-makefile/mllib1/src/test.ml4 b/test-suite/coq-makefile/mllib1/src/test.ml4
deleted file mode 100644
index 8ddc9b095..000000000
--- a/test-suite/coq-makefile/mllib1/src/test.ml4
+++ /dev/null
@@ -1,13 +0,0 @@
-DECLARE PLUGIN "test_plugin"
-let () = Mltop.add_known_plugin (fun () -> ()) "test_plugin";;
-
-VERNAC COMMAND EXTEND Test CLASSIFIED AS SIDEFF
-  | [ "Test" ] -> [ () ]
-END
-
-TACTIC EXTEND test
-| [ "test" ] -> [ Test_aux.tac ]
-END
-
-
-
diff --git a/test-suite/coq-makefile/mllib1/src/test.mli b/test-suite/coq-makefile/mllib1/src/test.mli
deleted file mode 100644
index e69de29bb..000000000
diff --git a/test-suite/coq-makefile/mllib1/src/test_aux.ml b/test-suite/coq-makefile/mllib1/src/test_aux.ml
deleted file mode 100644
index a01d0865a..000000000
--- a/test-suite/coq-makefile/mllib1/src/test_aux.ml
+++ /dev/null
@@ -1 +0,0 @@
-let tac = Proofview.tclUNIT ()
diff --git a/test-suite/coq-makefile/mllib1/src/test_aux.mli b/test-suite/coq-makefile/mllib1/src/test_aux.mli
deleted file mode 100644
index 10020f27d..000000000
--- a/test-suite/coq-makefile/mllib1/src/test_aux.mli
+++ /dev/null
@@ -1 +0,0 @@
-val tac : unit Proofview.tactic
diff --git a/test-suite/coq-makefile/mllib1/src/test_plugin.mllib b/test-suite/coq-makefile/mllib1/src/test_plugin.mllib
deleted file mode 100644
index cf94d851b..000000000
--- a/test-suite/coq-makefile/mllib1/src/test_plugin.mllib
+++ /dev/null
@@ -1,2 +0,0 @@
-Test_aux
-Test
diff --git a/test-suite/coq-makefile/mllib1/theories/test.v b/test-suite/coq-makefile/mllib1/theories/test.v
deleted file mode 100644
index 7753b56aa..000000000
--- a/test-suite/coq-makefile/mllib1/theories/test.v
+++ /dev/null
@@ -1,7 +0,0 @@
-Declare ML Module "test_plugin".
-Test.
-Goal True.
-Proof.
-test.
-exact I.
-Qed.
diff --git a/test-suite/coq-makefile/mlpack1/_CoqProject b/test-suite/coq-makefile/mlpack1/_CoqProject
index cb1ad4a4b..69f47302e 100644
--- a/test-suite/coq-makefile/mlpack1/_CoqProject
+++ b/test-suite/coq-makefile/mlpack1/_CoqProject
@@ -1,5 +1,5 @@
--R src/ test
--R theories/ test
+-R src test
+-R theories test
 -I src
 
 src/test_plugin.mlpack
diff --git a/test-suite/coq-makefile/mlpack1/run.sh b/test-suite/coq-makefile/mlpack1/run.sh
index 43d03be4a..418a2fb77 100755
--- a/test-suite/coq-makefile/mlpack1/run.sh
+++ b/test-suite/coq-makefile/mlpack1/run.sh
@@ -3,8 +3,8 @@
 #set -x
 set -e
 
-export PATH=../../../bin/:$PATH
-git clean -dfx .
+. ../template/init.sh
+
 coq_makefile -f _CoqProject -o Makefile
 make
 make html mlihtml
diff --git a/test-suite/coq-makefile/mlpack1/src/test.ml4 b/test-suite/coq-makefile/mlpack1/src/test.ml4
deleted file mode 100644
index 8ddc9b095..000000000
--- a/test-suite/coq-makefile/mlpack1/src/test.ml4
+++ /dev/null
@@ -1,13 +0,0 @@
-DECLARE PLUGIN "test_plugin"
-let () = Mltop.add_known_plugin (fun () -> ()) "test_plugin";;
-
-VERNAC COMMAND EXTEND Test CLASSIFIED AS SIDEFF
-  | [ "Test" ] -> [ () ]
-END
-
-TACTIC EXTEND test
-| [ "test" ] -> [ Test_aux.tac ]
-END
-
-
-
diff --git a/test-suite/coq-makefile/mlpack1/src/test.mli b/test-suite/coq-makefile/mlpack1/src/test.mli
deleted file mode 100644
index e69de29bb..000000000
diff --git a/test-suite/coq-makefile/mlpack1/src/test_aux.ml b/test-suite/coq-makefile/mlpack1/src/test_aux.ml
deleted file mode 100644
index a01d0865a..000000000
--- a/test-suite/coq-makefile/mlpack1/src/test_aux.ml
+++ /dev/null
@@ -1 +0,0 @@
-let tac = Proofview.tclUNIT ()
diff --git a/test-suite/coq-makefile/mlpack1/src/test_aux.mli b/test-suite/coq-makefile/mlpack1/src/test_aux.mli
deleted file mode 100644
index 10020f27d..000000000
--- a/test-suite/coq-makefile/mlpack1/src/test_aux.mli
+++ /dev/null
@@ -1 +0,0 @@
-val tac : unit Proofview.tactic
diff --git a/test-suite/coq-makefile/mlpack1/src/test_plugin.mlpack b/test-suite/coq-makefile/mlpack1/src/test_plugin.mlpack
deleted file mode 100644
index cf94d851b..000000000
--- a/test-suite/coq-makefile/mlpack1/src/test_plugin.mlpack
+++ /dev/null
@@ -1,2 +0,0 @@
-Test_aux
-Test
diff --git a/test-suite/coq-makefile/mlpack1/theories/test.v b/test-suite/coq-makefile/mlpack1/theories/test.v
deleted file mode 100644
index 7753b56aa..000000000
--- a/test-suite/coq-makefile/mlpack1/theories/test.v
+++ /dev/null
@@ -1,7 +0,0 @@
-Declare ML Module "test_plugin".
-Test.
-Goal True.
-Proof.
-test.
-exact I.
-Qed.
diff --git a/test-suite/coq-makefile/mlpack2/_CoqProject b/test-suite/coq-makefile/mlpack2/_CoqProject
new file mode 100644
index 000000000..51864a87a
--- /dev/null
+++ b/test-suite/coq-makefile/mlpack2/_CoqProject
@@ -0,0 +1,10 @@
+-R src/ test
+-R theories/ test
+-I src/
+
+src/test_plugin.mlpack
+src/test.ml4
+src/test.mli
+src/test_aux.ml
+src/test_aux.mli
+theories/test.v
diff --git a/test-suite/coq-makefile/mlpack2/run.sh b/test-suite/coq-makefile/mlpack2/run.sh
new file mode 100755
index 000000000..418a2fb77
--- /dev/null
+++ b/test-suite/coq-makefile/mlpack2/run.sh
@@ -0,0 +1,25 @@
+#!/bin/sh
+
+#set -x
+set -e
+
+. ../template/init.sh
+
+coq_makefile -f _CoqProject -o Makefile
+make
+make html mlihtml
+make install DSTROOT="$PWD/tmp"
+#make debug
+(cd `find tmp -name user-contrib`; find) | sort > actual
+sort > desired <<EOT
+.
+./test
+./test/test.glob
+./test/test_plugin.cmi
+./test/test_plugin.cmo
+./test/test_plugin.cmx
+./test/test_plugin.cmxs
+./test/test.v
+./test/test.vo
+EOT
+exec diff -u desired actual
diff --git a/test-suite/coq-makefile/multiroot/_CoqProject b/test-suite/coq-makefile/multiroot/_CoqProject
new file mode 100644
index 000000000..b384bb6d9
--- /dev/null
+++ b/test-suite/coq-makefile/multiroot/_CoqProject
@@ -0,0 +1,12 @@
+-R theories/ test
+-R theories2 test2
+-R src/ test
+-I src/
+
+./src/test_plugin.mllib
+./src/test.ml4
+./src/test.mli
+./src/test_aux.ml
+./src/test_aux.mli
+./theories/test.v
+./theories2/test.v
diff --git a/test-suite/coq-makefile/multiroot/run.sh b/test-suite/coq-makefile/multiroot/run.sh
new file mode 100755
index 000000000..a24a8a3cf
--- /dev/null
+++ b/test-suite/coq-makefile/multiroot/run.sh
@@ -0,0 +1,61 @@
+#!/bin/bash
+
+#set -x
+set -e
+
+. ../template/init.sh
+
+cp -r theories theories2
+mv src/test_plugin.mlpack src/test_plugin.mllib
+coq_makefile -f _CoqProject -o Makefile
+make
+make html mlihtml
+make install DSTROOT="$PWD/tmp"
+make install-doc DSTROOT="$PWD/tmp"
+#make debug
+(for d in `find tmp -name user-contrib`; do pushd $d >/dev/null; find; popd >/dev/null; done) | sort -u > actual
+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
+./test/test.vo
+./test2
+./test2/test.glob
+./test2/test.v
+./test2/test.vo
+./orphan_test_test2_test
+./orphan_test_test2_test/html
+./orphan_test_test2_test/html/coqdoc.css
+./orphan_test_test2_test/html/index.html
+./orphan_test_test2_test/html/test2.test.html
+./orphan_test_test2_test/html/test.test.html
+./orphan_test_test2_test/html/toc.html
+./orphan_test_test2_test/mlihtml
+./orphan_test_test2_test/mlihtml/index_attributes.html
+./orphan_test_test2_test/mlihtml/index_classes.html
+./orphan_test_test2_test/mlihtml/index_class_types.html
+./orphan_test_test2_test/mlihtml/index_exceptions.html
+./orphan_test_test2_test/mlihtml/index_extensions.html
+./orphan_test_test2_test/mlihtml/index.html
+./orphan_test_test2_test/mlihtml/index_methods.html
+./orphan_test_test2_test/mlihtml/index_modules.html
+./orphan_test_test2_test/mlihtml/index_module_types.html
+./orphan_test_test2_test/mlihtml/index_types.html
+./orphan_test_test2_test/mlihtml/index_values.html
+./orphan_test_test2_test/mlihtml/style.css
+./orphan_test_test2_test/mlihtml/Test_aux.html
+./orphan_test_test2_test/mlihtml/Test.html
+./orphan_test_test2_test/mlihtml/type_Test_aux.html
+./orphan_test_test2_test/mlihtml/type_Test.html
+EOT
+exec diff -u desired actual
diff --git a/test-suite/coq-makefile/native1/_CoqProject b/test-suite/coq-makefile/native1/_CoqProject
new file mode 100644
index 000000000..a6fa17348
--- /dev/null
+++ b/test-suite/coq-makefile/native1/_CoqProject
@@ -0,0 +1,11 @@
+-R src test
+-R theories test
+-I src
+-arg -native-compiler
+
+src/test_plugin.mlpack
+src/test.ml4
+src/test.mli
+src/test_aux.ml
+src/test_aux.mli
+theories/test.v
diff --git a/test-suite/coq-makefile/native1/run.sh b/test-suite/coq-makefile/native1/run.sh
new file mode 100755
index 000000000..097bd6398
--- /dev/null
+++ b/test-suite/coq-makefile/native1/run.sh
@@ -0,0 +1,34 @@
+#!/bin/sh
+
+#set -x
+set -e
+
+if which ocamlopt; then
+
+. ../template/init.sh
+	
+coq_makefile -f _CoqProject -o Makefile
+make
+make html mlihtml
+make install DSTROOT="$PWD/tmp"
+#make debug
+(cd `find tmp -name user-contrib`; find) | sort > actual
+sort > desired <<EOT
+.
+./test
+./test/test.glob
+./test/test_plugin.cmi
+./test/test_plugin.cmo
+./test/test_plugin.cmx
+./test/test_plugin.cmxs
+./test/test.v
+./test/test.vo
+./test/.coq-native
+./test/.coq-native/Ntest_test.cmi
+./test/.coq-native/Ntest_test.cmx
+./test/.coq-native/Ntest_test.cmxs
+EOT
+exec diff -u desired actual
+
+fi
+exit 0 # test skipped
diff --git a/test-suite/coq-makefile/plugin1/_CoqProject b/test-suite/coq-makefile/plugin1/_CoqProject
new file mode 100644
index 000000000..4eddc9d70
--- /dev/null
+++ b/test-suite/coq-makefile/plugin1/_CoqProject
@@ -0,0 +1,10 @@
+-R theories test
+-R src test
+-I src
+
+src/test_plugin.mllib
+src/test.ml4
+src/test.mli
+src/test_aux.ml
+src/test_aux.mli
+theories/test.v
diff --git a/test-suite/coq-makefile/plugin1/run.sh b/test-suite/coq-makefile/plugin1/run.sh
new file mode 100755
index 000000000..684e0ece8
--- /dev/null
+++ b/test-suite/coq-makefile/plugin1/run.sh
@@ -0,0 +1,31 @@
+#!/bin/sh
+
+#set -x
+set -e
+
+. ../template/init.sh
+
+mv src/test_plugin.mlpack src/test_plugin.mllib
+coq_makefile -f _CoqProject -o Makefile
+make
+make html mlihtml
+make install DSTROOT="$PWD/tmp"
+#make debug
+(cd `find tmp -name user-contrib`; find) | sort > actual
+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
+./test/test.vo
+EOT
+exec diff -u desired actual
diff --git a/test-suite/coq-makefile/plugin2/_CoqProject b/test-suite/coq-makefile/plugin2/_CoqProject
new file mode 100644
index 000000000..0bf1e07f2
--- /dev/null
+++ b/test-suite/coq-makefile/plugin2/_CoqProject
@@ -0,0 +1,10 @@
+-R theories/ test
+-R src/ test
+-I src/
+
+src/test_plugin.mllib
+src/test.ml4
+src/test.mli
+src/test_aux.ml
+src/test_aux.mli
+theories/test.v
diff --git a/test-suite/coq-makefile/plugin2/run.sh b/test-suite/coq-makefile/plugin2/run.sh
new file mode 100755
index 000000000..684e0ece8
--- /dev/null
+++ b/test-suite/coq-makefile/plugin2/run.sh
@@ -0,0 +1,31 @@
+#!/bin/sh
+
+#set -x
+set -e
+
+. ../template/init.sh
+
+mv src/test_plugin.mlpack src/test_plugin.mllib
+coq_makefile -f _CoqProject -o Makefile
+make
+make html mlihtml
+make install DSTROOT="$PWD/tmp"
+#make debug
+(cd `find tmp -name user-contrib`; find) | sort > actual
+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
+./test/test.vo
+EOT
+exec diff -u desired actual
diff --git a/test-suite/coq-makefile/plugin3/_CoqProject b/test-suite/coq-makefile/plugin3/_CoqProject
new file mode 100644
index 000000000..2028d49a8
--- /dev/null
+++ b/test-suite/coq-makefile/plugin3/_CoqProject
@@ -0,0 +1,10 @@
+-R theories/ test
+-R src/ test
+-I src/
+
+./src/test_plugin.mllib
+./src/test.ml4
+./src/test.mli
+./src/test_aux.ml
+./src/test_aux.mli
+./theories/test.v
diff --git a/test-suite/coq-makefile/plugin3/run.sh b/test-suite/coq-makefile/plugin3/run.sh
new file mode 100755
index 000000000..684e0ece8
--- /dev/null
+++ b/test-suite/coq-makefile/plugin3/run.sh
@@ -0,0 +1,31 @@
+#!/bin/sh
+
+#set -x
+set -e
+
+. ../template/init.sh
+
+mv src/test_plugin.mlpack src/test_plugin.mllib
+coq_makefile -f _CoqProject -o Makefile
+make
+make html mlihtml
+make install DSTROOT="$PWD/tmp"
+#make debug
+(cd `find tmp -name user-contrib`; find) | sort > actual
+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
+./test/test.vo
+EOT
+exec diff -u desired actual
diff --git a/test-suite/coq-makefile/template/init.sh b/test-suite/coq-makefile/template/init.sh
new file mode 100644
index 000000000..bfd2c1b95
--- /dev/null
+++ b/test-suite/coq-makefile/template/init.sh
@@ -0,0 +1,16 @@
+
+export PATH=../../../bin/:$PATH
+
+rm -rf theories src Makefile Makefile.conf tmp
+git clean -dfx || true
+
+mkdir -p src
+mkdir -p theories/sub
+
+cp ../template/theories/sub/testsub.v theories/sub
+cp ../template/theories/test.v theories
+cp ../template/src/test.ml4 src
+cp ../template/src/test_aux.mli src
+cp ../template/src/test.mli src
+cp ../template/src/test_plugin.mlpack src
+cp ../template/src/test_aux.ml src
diff --git a/test-suite/coq-makefile/template/src/test.ml4 b/test-suite/coq-makefile/template/src/test.ml4
new file mode 100644
index 000000000..72765abe0
--- /dev/null
+++ b/test-suite/coq-makefile/template/src/test.ml4
@@ -0,0 +1,14 @@
+open Ltac_plugin
+DECLARE PLUGIN "test_plugin"
+let () = Mltop.add_known_plugin (fun () -> ()) "test_plugin";;
+
+VERNAC COMMAND EXTEND Test CLASSIFIED AS SIDEFF
+  | [ "TestCommand" ] -> [ () ]
+END
+
+TACTIC EXTEND test
+| [ "test_tactic" ] -> [ Test_aux.tac ]
+END
+
+
+
diff --git a/test-suite/coq-makefile/template/src/test.mli b/test-suite/coq-makefile/template/src/test.mli
new file mode 100644
index 000000000..e69de29bb
diff --git a/test-suite/coq-makefile/template/src/test_aux.ml b/test-suite/coq-makefile/template/src/test_aux.ml
new file mode 100644
index 000000000..a01d0865a
--- /dev/null
+++ b/test-suite/coq-makefile/template/src/test_aux.ml
@@ -0,0 +1 @@
+let tac = Proofview.tclUNIT ()
diff --git a/test-suite/coq-makefile/template/src/test_aux.mli b/test-suite/coq-makefile/template/src/test_aux.mli
new file mode 100644
index 000000000..10020f27d
--- /dev/null
+++ b/test-suite/coq-makefile/template/src/test_aux.mli
@@ -0,0 +1 @@
+val tac : unit Proofview.tactic
diff --git a/test-suite/coq-makefile/template/src/test_plugin.mlpack b/test-suite/coq-makefile/template/src/test_plugin.mlpack
new file mode 100644
index 000000000..cf94d851b
--- /dev/null
+++ b/test-suite/coq-makefile/template/src/test_plugin.mlpack
@@ -0,0 +1,2 @@
+Test_aux
+Test
diff --git a/test-suite/coq-makefile/template/theories/sub/testsub.v b/test-suite/coq-makefile/template/theories/sub/testsub.v
new file mode 100644
index 000000000..755fc343f
--- /dev/null
+++ b/test-suite/coq-makefile/template/theories/sub/testsub.v
@@ -0,0 +1 @@
+Require Import test.
diff --git a/test-suite/coq-makefile/template/theories/test.v b/test-suite/coq-makefile/template/theories/test.v
new file mode 100644
index 000000000..744b5aad7
--- /dev/null
+++ b/test-suite/coq-makefile/template/theories/test.v
@@ -0,0 +1,7 @@
+Declare ML Module "test_plugin".
+TestCommand.
+Goal True.
+Proof.
+test_tactic.
+exact I.
+Qed.
diff --git a/test-suite/coq-makefile/uninstall1/_CoqProject b/test-suite/coq-makefile/uninstall1/_CoqProject
index 706cf75cc..35792066b 100644
--- a/test-suite/coq-makefile/uninstall1/_CoqProject
+++ b/test-suite/coq-makefile/uninstall1/_CoqProject
@@ -1,5 +1,5 @@
--R src/ test
--R theories/ test
+-R src test
+-R theories test
 -I src
 
 src/test_plugin.mlpack
diff --git a/test-suite/coq-makefile/uninstall1/run.sh b/test-suite/coq-makefile/uninstall1/run.sh
index a3bfe182b..d24176279 100755
--- a/test-suite/coq-makefile/uninstall1/run.sh
+++ b/test-suite/coq-makefile/uninstall1/run.sh
@@ -3,8 +3,8 @@
 #set -x
 set -e
 
-export PATH=../../../bin/:$PATH
-git clean -dfx .
+. ../template/init.sh
+
 coq_makefile -f _CoqProject -o Makefile
 make
 make html mlihtml
diff --git a/test-suite/coq-makefile/uninstall1/src/test.ml4 b/test-suite/coq-makefile/uninstall1/src/test.ml4
deleted file mode 100644
index 8ddc9b095..000000000
--- a/test-suite/coq-makefile/uninstall1/src/test.ml4
+++ /dev/null
@@ -1,13 +0,0 @@
-DECLARE PLUGIN "test_plugin"
-let () = Mltop.add_known_plugin (fun () -> ()) "test_plugin";;
-
-VERNAC COMMAND EXTEND Test CLASSIFIED AS SIDEFF
-  | [ "Test" ] -> [ () ]
-END
-
-TACTIC EXTEND test
-| [ "test" ] -> [ Test_aux.tac ]
-END
-
-
-
diff --git a/test-suite/coq-makefile/uninstall1/src/test.mli b/test-suite/coq-makefile/uninstall1/src/test.mli
deleted file mode 100644
index e69de29bb..000000000
diff --git a/test-suite/coq-makefile/uninstall1/src/test_aux.ml b/test-suite/coq-makefile/uninstall1/src/test_aux.ml
deleted file mode 100644
index a01d0865a..000000000
--- a/test-suite/coq-makefile/uninstall1/src/test_aux.ml
+++ /dev/null
@@ -1 +0,0 @@
-let tac = Proofview.tclUNIT ()
diff --git a/test-suite/coq-makefile/uninstall1/src/test_aux.mli b/test-suite/coq-makefile/uninstall1/src/test_aux.mli
deleted file mode 100644
index 10020f27d..000000000
--- a/test-suite/coq-makefile/uninstall1/src/test_aux.mli
+++ /dev/null
@@ -1 +0,0 @@
-val tac : unit Proofview.tactic
diff --git a/test-suite/coq-makefile/uninstall1/src/test_plugin.mlpack b/test-suite/coq-makefile/uninstall1/src/test_plugin.mlpack
deleted file mode 100644
index cf94d851b..000000000
--- a/test-suite/coq-makefile/uninstall1/src/test_plugin.mlpack
+++ /dev/null
@@ -1,2 +0,0 @@
-Test_aux
-Test
diff --git a/test-suite/coq-makefile/uninstall1/theories/sub/testsub.v b/test-suite/coq-makefile/uninstall1/theories/sub/testsub.v
deleted file mode 100644
index 755fc343f..000000000
--- a/test-suite/coq-makefile/uninstall1/theories/sub/testsub.v
+++ /dev/null
@@ -1 +0,0 @@
-Require Import test.
diff --git a/test-suite/coq-makefile/uninstall1/theories/test.v b/test-suite/coq-makefile/uninstall1/theories/test.v
deleted file mode 100644
index 7753b56aa..000000000
--- a/test-suite/coq-makefile/uninstall1/theories/test.v
+++ /dev/null
@@ -1,7 +0,0 @@
-Declare ML Module "test_plugin".
-Test.
-Goal True.
-Proof.
-test.
-exact I.
-Qed.
diff --git a/test-suite/coq-makefile/uninstall2/_CoqProject b/test-suite/coq-makefile/uninstall2/_CoqProject
new file mode 100644
index 000000000..d2a547d47
--- /dev/null
+++ b/test-suite/coq-makefile/uninstall2/_CoqProject
@@ -0,0 +1,11 @@
+-R src/ test
+-R theories/ test
+-I src/
+
+src/test_plugin.mlpack
+src/test.ml4
+src/test.mli
+src/test_aux.ml
+src/test_aux.mli
+theories/test.v
+theories/sub/testsub.v
diff --git a/test-suite/coq-makefile/uninstall2/run.sh b/test-suite/coq-makefile/uninstall2/run.sh
new file mode 100755
index 000000000..d24176279
--- /dev/null
+++ b/test-suite/coq-makefile/uninstall2/run.sh
@@ -0,0 +1,20 @@
+#!/bin/bash
+
+#set -x
+set -e
+
+. ../template/init.sh
+
+coq_makefile -f _CoqProject -o Makefile
+make
+make html mlihtml
+make install DSTROOT="$PWD/tmp"
+make install-doc DSTROOT="$PWD/tmp"
+make uninstall DSTROOT="$PWD/tmp"
+make uninstall-doc DSTROOT="$PWD/tmp"
+#make debug
+(for d in `find tmp -name user-contrib`; do pushd $d >/dev/null; find; popd >/dev/null; done) | sort -u > actual
+sort -u > desired <<EOT
+.
+EOT
+exec diff -u desired actual
diff --git a/test-suite/coq-makefile/validate1/_CoqProject b/test-suite/coq-makefile/validate1/_CoqProject
new file mode 100644
index 000000000..69f47302e
--- /dev/null
+++ b/test-suite/coq-makefile/validate1/_CoqProject
@@ -0,0 +1,10 @@
+-R src test
+-R theories test
+-I src
+
+src/test_plugin.mlpack
+src/test.ml4
+src/test.mli
+src/test_aux.ml
+src/test_aux.mli
+theories/test.v
diff --git a/test-suite/coq-makefile/validate1/run.sh b/test-suite/coq-makefile/validate1/run.sh
new file mode 100755
index 000000000..61025021d
--- /dev/null
+++ b/test-suite/coq-makefile/validate1/run.sh
@@ -0,0 +1,10 @@
+#!/bin/sh
+
+#set -x
+set -e
+
+. ../template/init.sh
+
+coq_makefile -f _CoqProject -o Makefile
+make
+exec make validate
-- 
cgit v1.2.3