Merge PR#406: coq makefile2

74 files changed, 2158 insertions, 1206 deletions

diff --git a/.gitignore b/.gitignore
index 371136fc7..c55ad24f8 100644
--- a/.gitignore
+++ b/.gitignore
@@ -60,6 +60,15 @@ test-suite/.nra.cache
 test-suite/trace
 test-suite/misc/universes/all_stdlib.v
 test-suite/misc/universes/universes.txt
+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-suite/coq-makefile/*/theories
+test-suite/coq-makefile/*/html
+test-suite/coq-makefile/*/mlihtml
+test-suite/coq-makefile/*/subdir/done
 
 # documentation
 
@@ -120,7 +129,7 @@ ide/xml_lexer.ml
 
 g_*.ml
 
-ide/project_file.ml
+lib/coqProject_file.ml
 parsing/cLexer.ml
 plugins/ltac/coretactics.ml
 plugins/ltac/extratactics.ml
diff --git a/.travis.yml b/.travis.yml
index a959fbf96..14bafd345 100644
--- a/.travis.yml
+++ b/.travis.yml
@@ -88,6 +88,7 @@ matrix:
           - ghostscript
           - transfig
           - imagemagick
+          - tipa
 
     - env:
       - TEST_TARGET="test-suite"
diff --git a/CHANGES b/CHANGES
index 31d691be0..0b55183f3 100644
--- a/CHANGES
+++ b/CHANGES
@@ -54,6 +54,22 @@ Dependencies
 
 - Support for camlp4 has been removed.
 
+Tools
+
+- coq_makefile was completely redesigned to improve its maintainability and
+  the extensibility of generated Makefiles, and to make _CoqProject files
+  more palatable to IDEs.  Overview:
+  * _CoqProject files contain only Coq specific data (i.e. the list of
+    files, -R options, ...)
+  * coq_makefile translates _CoqProject to Makefile.conf and copies in the
+    desired location a standard Makefile (that reads Makefile.conf)
+  * Makefile extensions can be implemented in a Makefile.local file (read
+    by the main Makefile) by installing a hook in the extension points
+    provided by the standard Makefile
+  The current version contains code for retro compatibility that prints
+  warnings when a deprecated feature is used.  Please upgrade your _CoqProject
+  accordingly.
+
 Changes from V8.6beta1 to V8.6
 ==============================
 
diff --git a/Makefile b/Makefile
index 826ed17b0..7ba2c80f1 100644
--- a/Makefile
+++ b/Makefile
@@ -54,6 +54,7 @@ FIND_VCS_CLAUSE:='(' \
   -name "$${GIT_DIR}" -o \
   -name '_build' -o \
   -name '_build_ci' \
+  -name 'coq-makefile' \
 ')' -prune -o
 
 define find
diff --git a/Makefile.build b/Makefile.build
index 56f1fb8b4..8aedd9cec 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -377,7 +377,7 @@ $(GALLINA): $(call bestobj, tools/gallina_lexer.cmo tools/gallina.cmo)
 	$(SHOW)'OCAMLBEST -o $@'
 	$(HIDE)$(call bestocaml,,)
 
-COQMAKEFILECMO:=lib/clib.cma ide/project_file.cmo tools/coq_makefile.cmo
+COQMAKEFILECMO:=lib/clib.cma tools/coq_makefile.cmo
 
 $(COQMAKEFILE): $(call bestobj,$(COQMAKEFILECMO))
 	$(SHOW)'OCAMLBEST -o $@'
diff --git a/Makefile.install b/Makefile.install
index bde035551..33f881c11 100644
--- a/Makefile.install
+++ b/Makefile.install
@@ -96,6 +96,7 @@ install-devfiles:
 	$(MKDIR) $(FULLCOQLIB)
 	$(INSTALLSH)  $(FULLCOQLIB) $(LINKCMO) $(GRAMMARCMA)
 	$(INSTALLSH)  $(FULLCOQLIB) $(INSTALLCMI)
+	$(INSTALLSH)  $(FULLCOQLIB) tools/CoqMakefile.in
 ifeq ($(BEST),opt)
 	$(INSTALLSH)  $(FULLCOQLIB) $(LINKCMX) $(CORECMA:.cma=.a) $(STATICPLUGINS:.cma=.a)
 endif
diff --git a/configure.ml b/configure.ml
index 679f52417..7af18cb85 100644
--- a/configure.ml
+++ b/configure.ml
@@ -897,7 +897,7 @@ let do_one_instdir (var,msg,r,dflt,suff) =
 
 let do_one_noinst (var,msg,_,_,_) =
   if var="CONFIGDIR" || var="DATADIR" then (var,msg,coqtop^"/ide",true)
-  else (var,msg,"",false)
+  else (var,msg,coqtop^"/doc",false)
 
 let install_dirs =
   let f = if !Prefs.local then do_one_noinst else do_one_instdir in
diff --git a/dev/ci/ci-user-overlay.sh b/dev/ci/ci-user-overlay.sh
index 28808a581..71d098e37 100644
--- a/dev/ci/ci-user-overlay.sh
+++ b/dev/ci/ci-user-overlay.sh
@@ -40,3 +40,9 @@ if [ $TRAVIS_PULL_REQUEST == "402" ] || [ $TRAVIS_BRANCH == "located_switch" ];
     bedrock_facade_CI_GITURL=https://github.com/ejgallego/bedrock.git
 
 fi
+
+if [ $TRAVIS_PULL_REQUEST == "406" ] || [ $TRAVIS_BRANCH == "feature/coq_makefile2" ]; then
+    UniMath_CI_BRANCH=master
+    UniMath_CI_GITURL=https://github.com/gares/UniMath.git
+fi
+
diff --git a/doc/refman/RefMan-uti.tex b/doc/refman/RefMan-uti.tex
index 9962ce996..08cdbee50 100644
--- a/doc/refman/RefMan-uti.tex
+++ b/doc/refman/RefMan-uti.tex
@@ -51,6 +51,95 @@ arguments. In other cases, the debugger is simply called without additional
 arguments. Such a wrapper can be found in the \texttt{dev/}
 subdirectory of the sources.
 
+\section[Building a \Coq\ project with {\tt coq\_makefile}]
+{Building a \Coq\ project with {\tt coq\_makefile}
+\label{Makefile}
+\ttindex{Makefile}
+\ttindex{coq\_Makefile}
+\ttindex{\_CoqProject}}
+
+The majority of \Coq\ projects are very similar: a collection of {\tt .v}
+files and eventually some {\tt .ml} ones (a \Coq\ plugin).  The main piece
+of metadata needed in order to build the project are the command 
+line options to {\tt coqc} (e.g. {\tt -R, -I},
+\SeeAlso Section~\ref{coqoptions}). Collecting the list of files and
+options is the job of the {\tt \_CoqProject} file.
+
+A simple example of a {\tt \_CoqProject} file follows:
+
+\begin{verbatim}
+-R theories/ MyCode
+theories/foo.v
+theories/bar.v
+-I src/
+src/baz.ml4
+src/bazaux.ml
+src/qux_plugin.mlpack
+\end{verbatim}
+
+Currently, both \CoqIDE{} and Proof General (version $\geq$ 4.3pre) understand
+{\tt \_CoqProject} files and invoke \Coq\ with the desired options.
+
+The {\tt coq\_makefile} utility can be used to set up a build infrastructure
+for the \Coq\ project based on makefiles.  The recommended way of
+invoking {\tt coq\_makefile} is the following one:
+
+\begin{verbatim}
+coq_makefile -f _CoqProject -o CoqMakefile
+\end{verbatim}
+
+Such command generates the following files:
+\begin{description}
+	\item[{\tt CoqMakefile}] is a generic makefile for GNU Make that provides targets to build the project (both {\tt .v} and {\tt .ml*} files), to install it system-wide in the {\tt coq-contrib} directory (i.e. where \Coq\ is installed) as well as to invoke {\tt coqdoc} to generate html documentation.
+
+	\item[{\tt CoqMakefile.conf}] contains make variables assignments that reflect the contents of the {\tt \_CoqProject} file as well as the path relevant to \Coq{}.
+\end{description}
+
+An optional file {\bf {\tt CoqMakefile.local}} can be provided by the user in order to extend {\tt CoqMakefile}.  In particular one can declare custom actions to be performed before or after the build process. Similarly one can customize the install target or even provide new targets.  Extension points are documented in the {\tt CoqMakefile} file.
+
+The extensions of the files listed in {\tt \_CoqProject} is
+used in order to decide how to build them  In particular:
+
+\begin{itemize}
+\item {\Coq} files must use the \texttt{.v} extension
+\item {\ocaml} files must use the \texttt{.ml} or \texttt{.mli} extension
+\item {\ocaml} files that require pre processing for syntax extensions (like {\tt VERNAC EXTEND}) must use the \texttt{.ml4} extension
+\item In order to generate a plugin one has to list all {\ocaml} modules (i.e. ``Baz'' for ``baz.ml'') in a \texttt{.mlpack} file (or \texttt{.mllib} file).
+\end{itemize}
+
+The use of \texttt{.mlpack} files has to be preferred over \texttt{.mllib}
+files, since it results in a ``packed'' plugin: All auxiliary 
+modules (as {\tt Baz} and {\tt Bazaux}) are hidden inside
+the plugin's ``name space'' ({\tt Qux\_plugin}).
+This reduces the chances of begin unable to load two distinct plugins
+because of a clash in their auxiliary module names.
+
+\paragraph{Notes about including the generated Makefile}
+
+This practice is discouraged. The contents of this file, including variable names
+and status of rules shall change in the future.  Users are advised to
+include {\tt Makefile.conf} or call a target of the generated Makefile
+as in {\tt make -f Makefile target} from another Makefile.
+
+\paragraph{Notes for users of {\tt coq\_makefile} with version $<$ 8.7}
+
+\begin{itemize}
+\item Support for ``sub-directory'' is deprecated.  To perform actions before
+	or after the build (like invoking make on a subdirectory) one can
+	hook in {\tt pre-all} and {\tt post-all} extension points
+\item \texttt{-extra-phony} and \texttt{-extra} are deprecated.  To provide
+	additional target ({\tt .PHONY} or not) please use 
+	{\tt CoqMakefile.local}
+\end{itemize}
+
+\paragraph{Note: building a subset of the targets with -j}
+
+To build, say, two targets \texttt{foo.vo} and \texttt{bar.vo}
+in parallel one can use \texttt{make only TGTS="foo.vo bar.vo" -j}.
+
+Note that \texttt{make foo.vo bar.vo -j} has a different meaning for
+the make utility, in particular it may build a shared prerequisite twice.
+
 \section[Modules dependencies]{Modules dependencies\label{Dependencies}\index{Dependencies}
   \ttindex{coqdep}}
 
@@ -73,110 +162,9 @@ instead for the \ocaml\ modules dependencies.
 
 See the man page of {\tt coqdep} for more details and options.
 
-
-\section[Creating a {\tt Makefile} for \Coq\ modules]
-{Creating a {\tt Makefile} for \Coq\ modules
-\label{Makefile}
-\ttindex{Makefile}
-\ttindex{coq\_Makefile}
-\ttindex{\_CoqProject}}
-
-A project is a proof development split into several files, possibly
-including the sources of some {\ocaml} plugins, that are located (in
-various sub-directories of) a certain directory. The
-\texttt{coq\_makefile} command allows to generate generic and complete
-\texttt{Makefile} files, that can be used to compile the different
-components of the project. A \_CoqProject file
-specifies both the list of target files relevant to the project
-and the common options that should be passed to each executable at
-compilation times, for the IDE, etc.
-
-\paragraph{\_CoqProject file as an argument to  coq\_Makefile.}
-In particular, a \_CoqProject file contains the relevant
-arguments to be passed to the \texttt{coq\_makefile} makefile
-generator using for instance the command:
-
-\begin{quotation}
-\texttt{\% coq\_makefile -f \_CoqProject -o Makefile}
-\end{quotation}
-
-This command generates a file \texttt{Makefile} that can be used to
-compile all the sources of the current project. It follows the
-syntax described by the output of \texttt{\% coq\_makefile -{}-help}.
-Once the \texttt{Makefile} file has been generated a first time, it
-can be used by the \texttt{make} command to compile part or all of
-the project. Note that once it has been generated once, as soon as
-\texttt{\_CoqProject} file is updated, the \texttt{Makefile} file is
-automatically regenerated by an invocation of \texttt{make}.
-
-The following command generates a minimal example of
-\texttt{\_CoqProject} file:
-\begin{quotation}
-\texttt{\% ( echo "-R .\ }\textit{MyFancyLib}\texttt{" ; find .\ -name
-  "*.v" -print ) > \_CoqProject}
-\end{quotation}
-when executed at the root of the directory containing the
-project. Here the \texttt{\_CoqProject} lists all the \texttt{.v} files
-that are present in the current directory and its sub-directories. But no
-plugin sources is listed. If a \texttt{Makefile} is generated from
-this \texttt{\_CoqProject}, the command \texttt{make install} will
-install the compiled project in a sub-directory \texttt{MyFancyLib} of
-the \texttt{user-contrib} directory  (of the user's {\Coq} libraries
-location). This sub-directory is created if it does not already exist.
-
-\paragraph{\_CoqProject file as a configuration for IDEs.}
-
-A \texttt{\_CoqProject} file can also be used to configure the options
-of the \texttt{coqtop} process executed by a user interface. This
-allows to import the libraries of the project under a correct name,
-both as a developer of the project, working in the directory
-containing its sources, and as a user, using the project after
-the installation of its libraries. Currently, both \CoqIDE{} and Proof
-General (version $\geq$ 4.3pre) support configuration via
-\texttt{\_CoqProject} files.
-
-\paragraph{Remarks.}
-
-\begin{itemize}
-\item Every {\Coq} files must use a \texttt{.v} file extension.
- The {\ocaml} modules must use a \texttt{.ml4} file extension
- if they require camlp preprocessing (and in \texttt{.ml} otherwise).
- The {\ocaml} module signatures, library
- description and packing files must use respectively \texttt{.mli},
- \texttt{.mllib} and \texttt{.mlpack} file extension.
-
-\item Any argument that is not a valid option is considered as a
-  sub-directory. Any sub-directory specified in the list of targets must
-  itself contain a \texttt{Makefile}.
-
-\item The phony targets \texttt{all} and \texttt{clean} recursively
-  call their target in every sub-directory.
-
-\item \texttt{-R} and \texttt{-Q} options are for {\Coq} files, \texttt{-I}
-  for {\ocaml} ones. A same directory can be passed to both nature of
-  options, in the same \texttt{\_CoqProject}.
-
-\item Using \texttt{-R} or \texttt{-Q} is the appropriate way to
-  obtain both a correct logical path and a correct installation location to
-  the libraries of a given project.
-
-\item Dependencies on external libraries to the project must be
-  declared with care. If in the \texttt{\_CoqProject} file an external
-  library \texttt{foo} is passed to a \texttt{-Q} option, like in
-  \texttt{-Q foo}, the subsequent \textit{make clean} command can
-  erase \textit{foo}. It is hence safer to customize the
-  \texttt{COQPATH} variable (see \ref{envars}), to include the
-  location of the required external libraries.
-
-\item Using \texttt{-extra-phony} with no command adds extra
-  dependencies on already defined rules. For example the following
-  skeleton appends ``something'' to the \texttt{install} rule:
-\begin{quotation}
-\texttt{-extra-phony "install" "install-my-stuff" ""
-  -extra-phony "install-my-stuff" "" "something"}
-\end{quotation}
-\end{itemize}
-
+The build infrastructure generated by {\tt coq\_makefile}
+uses {\tt coqdep} to automatically compute the dependencies
+among the files part of the project.
 
 \section[Documenting \Coq\ files with coqdoc]{Documenting \Coq\ files with coqdoc\label{coqdoc}
 \ttindex{coqdoc}}
diff --git a/ide/coqide.ml b/ide/coqide.ml
index 663e28d36..a1e78ee3c 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -46,7 +46,7 @@ open Session
 
 (** The arguments that will be passed to coqtop. No quoting here, since
     no /bin/sh when using create_process instead of open_process. *)
-let custom_project_files = ref []
+let custom_project_file = ref None
 let sup_args = ref []
 
 let logfile = ref None
@@ -81,17 +81,27 @@ let pr_exit_status = function
   | Unix.WEXITED 0 -> " succeeded"
   | _ -> " failed"
 
-let make_coqtop_args = function
-  |None -> "", !sup_args
-  |Some the_file ->
-    let get_args f = Project_file.args_from_project f
-      !custom_project_files project_file_name#get
-    in
-    match read_project#get with
-      |Ignore_args -> "", !sup_args
-      |Append_args ->
-         let fname, args = get_args the_file in fname, args @ !sup_args
-      |Subst_args -> get_args the_file
+let make_coqtop_args fname =
+  let open CoqProject_file in
+  let base_args = match read_project#get with
+    | Ignore_args -> !sup_args
+    | Append_args -> !sup_args
+    | Subst_args -> [] in
+  if read_project#get = Ignore_args then "", base_args
+  else
+    match !custom_project_file, fname with
+    | Some (d,proj), _ -> d, coqtop_args_from_project proj @ base_args
+    | None, None -> "", base_args
+    | None, Some the_file ->
+       match
+         CoqProject_file.find_project_file
+           ~from:(Filename.dirname the_file)
+           ~projfile_name:project_file_name#get
+       with
+       | None -> "", base_args
+       | Some proj -> 
+           proj, coqtop_args_from_project (read_project_file proj) @ base_args
+;;
 
 (** Setting drag & drop on widgets *)
 
@@ -1345,9 +1355,11 @@ let read_coqide_args argv =
       if coqtop = None then filter_coqtop (Some prog) project_files out args
       else (output_string stderr "Error: multiple -coqtop options"; exit 1)
     |"-f" :: file :: args ->
+      if project_files <> None then
+        (output_string stderr "Error: multiple -f options"; exit 1);
       let d = CUnix.canonical_path_name (Filename.dirname file) in
-      let p = Project_file.read_project_file file in
-      filter_coqtop coqtop ((d,p) :: project_files) out args
+      let p = CoqProject_file.read_project_file file in
+      filter_coqtop coqtop (Some (d,p)) out args
     |"-f" :: [] ->
       output_string stderr "Error: missing project file name"; exit 1
     |"-coqtop" :: [] ->
@@ -1364,11 +1376,11 @@ let read_coqide_args argv =
       (* argument added by MacOS during .app launch *)
       filter_coqtop coqtop project_files out args
     |arg::args -> filter_coqtop coqtop project_files (arg::out) args
-    |[] -> (coqtop,List.rev project_files,List.rev out)
+    |[] -> (coqtop,project_files,List.rev out)
   in
-  let coqtop,project_files,argv = filter_coqtop None [] [] argv in
+  let coqtop,project_files,argv = filter_coqtop None None [] argv in
   Ideutils.custom_coqtop := coqtop;
-  custom_project_files := project_files;
+  custom_project_file := project_files;
   argv
 
 
diff --git a/ide/ide.mllib b/ide/ide.mllib
index 78b4c01e8..57e9fe5ad 100644
--- a/ide/ide.mllib
+++ b/ide/ide.mllib
@@ -9,6 +9,8 @@ Config_lexer
 Utf8_convert
 Preferences
 Project_file
+Serialize
+Richprinter
 Xml_lexer
 Xml_parser
 Xml_printer
diff --git a/ide/project_file.ml4 b/ide/project_file.ml4
deleted file mode 100644
index de0720e03..000000000
--- a/ide/project_file.ml4
+++ /dev/null
@@ -1,202 +0,0 @@
-type target =
-  | ML of string (* ML file : foo.ml -> (ML "foo.ml") *)
-  | MLI of string (* MLI file : foo.mli -> (MLI "foo.mli") *)
-  | ML4 of string (* ML4 file : foo.ml4 -> (ML4 "foo.ml4") *)
-  | MLLIB of string (* MLLIB file : foo.mllib -> (MLLIB "foo.mllib") *)
-  | MLPACK of string (* MLLIB file : foo.mlpack -> (MLLIB "foo.mlpack") *)
-  | V of string  (* V file : foo.v -> (V "foo") *)
-  | Arg of string
-  | Special of string * string * bool * string
-    (* file, dependencies, is_phony, command *)
-  | Subdir of string
-  | Def of string * string (* X=foo -> Def ("X","foo") *)
-  | MLInclude of string (* -I physicalpath *)
-  | Include of string * string (* -Q physicalpath logicalpath *)
-  | RInclude of string * string (* -R physicalpath logicalpath *)
-
-type install =
-  | NoInstall
-  | TraditionalInstall
-  | UserInstall
-  | UnspecInstall
-
-exception Parsing_error
-let rec parse_string = parser
-  | [< '' ' | '\n' | '\t' >] -> ""
-  | [< 'c; s >] -> (String.make 1 c)^(parse_string s)
-  | [< >] -> ""
-and parse_string2 = parser
-  | [< ''"' >] -> ""
-  | [< 'c; s >] -> (String.make 1 c)^(parse_string2 s)
-  | [< >] -> raise Parsing_error
-and parse_skip_comment = parser
-  | [< ''\n'; s >] -> s
-  | [< 'c; s >] -> parse_skip_comment s
-  | [< >] -> [< >]
-and parse_args = parser
-  | [< '' ' | '\n' | '\t'; s >] -> parse_args s
-  | [< ''#'; s >] -> parse_args (parse_skip_comment s)
-  | [< ''"'; str = parse_string2; s >] -> ("" ^ str) :: parse_args s
-  | [< 'c; str = parse_string; s >] -> ((String.make 1 c) ^ str) :: (parse_args s)
-  | [< >] -> []
-
-
-let parse f =
-  let c = open_in f in
-  let res = parse_args (Stream.of_channel c) in
-    close_in c;
-    res
-
-let rec process_cmd_line orig_dir ((project_file,makefile,install,opt) as opts) l = function
-  | [] -> opts, l
-  | ("-h"|"--help") :: _ ->
-    raise Parsing_error
-  | ("-no-opt"|"-byte") :: r ->
-    process_cmd_line orig_dir (project_file,makefile,install,false) l r
-  | ("-full"|"-opt") :: r ->
-    process_cmd_line orig_dir (project_file,makefile,install,true) l r
-  | "-impredicative-set" :: r ->
-    Feedback.msg_warning (Pp.str "Please now use \"-arg -impredicative-set\" instead of \"-impredicative-set\" alone to be more uniform.");
-    process_cmd_line orig_dir opts (Arg "-impredicative-set" :: l) r
-  | "-no-install" :: r ->
-    Feedback.msg_warning (Pp.(++) (Pp.str "Option -no-install is deprecated.") (Pp.(++) (Pp.spc ()) (Pp.str "Use \"-install none\" instead")));
-    process_cmd_line orig_dir (project_file,makefile,NoInstall,opt) l r
-  | "-install" :: d :: r ->
-    if install <> UnspecInstall then Feedback.msg_warning (Pp.str "-install sets more than once.");
-    let install =
-      match d with
-	| "user" -> UserInstall
-	| "none" -> NoInstall
-	| "global" -> TraditionalInstall
-	| _ -> Feedback.msg_warning (Pp.(++) (Pp.str "invalid option '") (Pp.(++) (Pp.str d) (Pp.str "' passed to -install.")));
-          install
-    in
-    process_cmd_line orig_dir (project_file,makefile,install,opt) l r
-  | "-custom" :: com :: dependencies :: file :: r ->
-    Feedback.msg_warning (Pp.app
-    (Pp.str "Please now use \"-extra[-phony] result deps command\" instead of \"-custom command deps result\".")
-    (Pp.pr_arg Pp.str "It follows makefile target declaration order and has a clearer semantic.")
-    );
-    process_cmd_line orig_dir opts (Special (file,dependencies,false,com) :: l) r
-  | "-extra" :: file :: dependencies :: com :: r ->
-    process_cmd_line orig_dir opts (Special (file,dependencies,false,com) :: l) r
-  | "-extra-phony" :: target :: dependencies :: com :: r ->
-    process_cmd_line orig_dir opts (Special (target,dependencies,true,com) :: l) r
-  | "-Q" :: d :: lp :: r ->
-    process_cmd_line orig_dir opts ((Include (CUnix.correct_path d orig_dir, lp)) :: l) r
-  | "-I" :: d :: r ->
-    process_cmd_line orig_dir opts ((MLInclude (CUnix.correct_path d orig_dir)) :: l) r
-  | "-R" :: p :: lp :: r ->
-    process_cmd_line orig_dir opts (RInclude (CUnix.correct_path p orig_dir,lp) :: l) r
-  | ("-Q"|"-R"|"-I"|"-custom"|"-extra"|"-extra-phony") :: _ ->
-    raise Parsing_error
-  | "-f" :: file :: r ->
-    let file = CUnix.remove_path_dot (CUnix.correct_path file orig_dir) in
-    let () = match project_file with
-      | None -> ()
-      | Some _ -> Feedback.msg_warning (Pp.str
-	"Several features will not work with multiple project files.")
-    in
-    let (opts',l') = process_cmd_line (Filename.dirname file) (Some file,makefile,install,opt) l (parse file) in
-      process_cmd_line orig_dir opts' l' r
-  | ["-f"] ->
-    raise Parsing_error
-  | "-o" :: file :: r ->
-      begin try
-	let _ = String.index file '/' in
-	  raise Parsing_error
-      with Not_found ->
-	let () = match makefile with
-	  |None -> ()
-	  |Some f ->
-	     Feedback.msg_warning (Pp.(++) (Pp.str "Only one output file is genererated. ") (Pp.(++) (Pp.str f) (Pp.str " will not be.")))
-	in process_cmd_line orig_dir (project_file,Some file,install,opt) l r
-      end
-  | v :: "=" :: def :: r ->
-    process_cmd_line orig_dir opts (Def (v,def) :: l) r
-  | "-arg" :: a :: r ->
-    process_cmd_line orig_dir opts (Arg a :: l) r
-  | f :: r ->
-      let f = CUnix.correct_path f orig_dir in
-	process_cmd_line orig_dir opts ((
-          if Filename.check_suffix f ".v" then V f
-	  else if (Filename.check_suffix f ".ml") then ML f
-	  else if (Filename.check_suffix f ".ml4") then ML4 f
-	  else if (Filename.check_suffix f ".mli") then MLI f
-	  else if (Filename.check_suffix f ".mllib") then MLLIB f
-	  else if (Filename.check_suffix f ".mlpack") then MLPACK f
-	  else Subdir f) :: l) r
-
-let process_cmd_line orig_dir opts l args =
-  let (opts, l) = process_cmd_line orig_dir opts l args in
-  opts, List.rev l
-
-let rec post_canonize f =
-  if Filename.basename f = Filename.current_dir_name
-  then let dir = Filename.dirname f in
-    if dir = Filename.current_dir_name then f else post_canonize dir
-  else f
-
-(* Return: ((v,(mli,ml4,ml,mllib,mlpack),special,subdir),(ml_inc,q_inc,r_inc),(args,defs)) *)
-let split_arguments args =
-  List.fold_right
-    (fun a ((v,(mli,ml4,ml,mllib,mlpack as m),o,s as t),
-            (ml_inc,q_inc,r_inc as i),(args,defs as d)) ->
-     match a with
-     | V n ->
-        ((CUnix.remove_path_dot n::v,m,o,s),i,d)
-     | ML n ->
-        ((v,(mli,ml4,CUnix.remove_path_dot n::ml,mllib,mlpack),o,s),i,d)
-     | MLI n ->
-        ((v,(CUnix.remove_path_dot n::mli,ml4,ml,mllib,mlpack),o,s),i,d)
-     | ML4 n ->
-        ((v,(mli,CUnix.remove_path_dot n::ml4,ml,mllib,mlpack),o,s),i,d)
-     | MLLIB n ->
-        ((v,(mli,ml4,ml,CUnix.remove_path_dot n::mllib,mlpack),o,s),i,d)
-     | MLPACK n ->
-        ((v,(mli,ml4,ml,mllib,CUnix.remove_path_dot n::mlpack),o,s),i,d)
-     | Special (n,dep,is_phony,c) ->
-        ((v,m,(n,dep,is_phony,c)::o,s),i,d)
-     | Subdir n ->
-        ((v,m,o,n::s),i,d)
-     | MLInclude p ->
-        let ml_new = (CUnix.remove_path_dot (post_canonize p),
-                      CUnix.canonical_path_name p) in
-        (t,(ml_new::ml_inc,q_inc,r_inc),d)
-     | Include (p,l) ->
-        let q_new = (CUnix.remove_path_dot (post_canonize p),l,
-		     CUnix.canonical_path_name p) in
-        (t,(ml_inc,q_new::q_inc,r_inc),d)
-     | RInclude (p,l) ->
-        let r_new = (CUnix.remove_path_dot (post_canonize p),l,
-		     CUnix.canonical_path_name p) in
-        (t,(ml_inc,q_inc,r_new::r_inc),d)
-     | Def (v,def) ->
-        (t,i,(args,(v,def)::defs))
-     | Arg a ->
-        (t,i,(a::args,defs)))
-    args (([],([],[],[],[],[]),[],[]),([],[],[]),([],[]))
-
-let read_project_file f =
-  split_arguments
-    (snd (process_cmd_line (Filename.dirname f) (Some f, None, NoInstall, true) [] (parse f)))
-
-let args_from_project file project_files default_name =
-  let build_cmd_line ml_inc i_inc r_inc args =
-    List.fold_right (fun (_,i) o -> "-I" :: i :: o) ml_inc
-      (List.fold_right (fun (_,l,i) o -> "-Q" :: i :: l :: o) i_inc
-        (List.fold_right (fun (_,l,p) o -> "-R" :: p :: l :: o) r_inc
-	  (List.fold_right (fun a o -> parse_args (Stream.of_string a) @ o) args [])))
-  in try
-      let (fname,(_,(ml_inc,i_inc,r_inc),(args,_))) = List.hd project_files in
-	fname, build_cmd_line ml_inc i_inc r_inc args
-    with Failure _ ->
-      let rec find_project_file dir = try
-	let fname = Filename.concat dir default_name in
-	let ((v_files,_,_,_),(ml_inc,i_inc,r_inc),(args,_)) =
-          read_project_file fname in
-	fname, build_cmd_line ml_inc i_inc r_inc args
-      with Sys_error s ->
-	let newdir = Filename.dirname dir in
-	  if dir = newdir then "",[] else find_project_file newdir
-      in find_project_file (Filename.dirname file)
diff --git a/lib/clib.mllib b/lib/clib.mllib
index 9eb479fcc..d5c938fe5 100644
--- a/lib/clib.mllib
+++ b/lib/clib.mllib
@@ -33,3 +33,4 @@ CUnix
 Envars
 Aux_file
 Monad
+CoqProject_file
diff --git a/lib/coqProject_file.ml4 b/lib/coqProject_file.ml4
new file mode 100644
index 000000000..7a1660569
--- /dev/null
+++ b/lib/coqProject_file.ml4
@@ -0,0 +1,215 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+type project = {
+  project_file  : string option;
+  makefile : string option;
+  install_kind  : install option;
+  use_ocamlopt : bool;
+
+  v_files : string list;
+  mli_files : string list;
+  ml4_files : string list;
+  ml_files : string list;
+  mllib_files : string list;
+  mlpack_files : string list;
+
+  ml_includes : path list;
+  r_includes  : (path * logic_path) list;
+  q_includes  : (path * logic_path) list;
+  extra_args : string list;
+  defs : (string * string) list;
+  
+  extra_targets : extra_target list;
+  subdirs : string list;
+}
+and extra_target = {
+  target : string;
+  dependencies : string;
+  phony : bool;
+  command : string;
+}
+and logic_path = string
+and path = { path : string; canonical_path : string }
+and install =
+  | NoInstall
+  | TraditionalInstall
+  | UserInstall
+
+(* TODO generate with PPX *)
+let mk_project project_file makefile install_kind use_ocamlopt = {
+  project_file;
+  makefile;
+  install_kind;
+  use_ocamlopt;
+
+  v_files = [];
+  mli_files = [];
+  ml4_files = [];
+  ml_files = [];
+  mllib_files = [];
+  mlpack_files = [];
+  extra_targets = [];
+  subdirs = [];
+  ml_includes = [];
+  r_includes = [];
+  q_includes = [];
+  extra_args = [];
+  defs = [];
+}
+
+(********************* utils ********************************************)
+
+let rec post_canonize f =
+  if Filename.basename f = Filename.current_dir_name
+  then let dir = Filename.dirname f in
+    if dir = Filename.current_dir_name then f else post_canonize dir
+  else f
+
+(* Avoid Sys.is_directory raise an exception (if the file does not exists) *)
+let is_directory f = Sys.file_exists f && Sys.is_directory f
+
+(********************* parser *******************************************)
+
+exception Parsing_error of string
+
+let rec parse_string = parser
+  | [< '' ' | '\n' | '\t' >] -> ""
+  | [< 'c; s >] -> (String.make 1 c)^(parse_string s)
+  | [< >] -> ""
+and parse_string2 = parser
+  | [< ''"' >] -> ""
+  | [< 'c; s >] -> (String.make 1 c)^(parse_string2 s)
+  | [< >] -> raise (Parsing_error "unterminated string")
+and parse_skip_comment = parser
+  | [< ''\n'; s >] -> s
+  | [< 'c; s >] -> parse_skip_comment s
+  | [< >] -> [< >]
+and parse_args = parser
+  | [< '' ' | '\n' | '\t'; s >] -> parse_args s
+  | [< ''#'; s >] -> parse_args (parse_skip_comment s)
+  | [< ''"'; str = parse_string2; s >] -> ("" ^ str) :: parse_args s
+  | [< 'c; str = parse_string; s >] -> ((String.make 1 c) ^ str) :: (parse_args s)
+  | [< >] -> []
+
+let parse f =
+  let c = open_in f in
+  let res = parse_args (Stream.of_channel c) in
+  close_in c;
+  res
+;;
+
+let process_cmd_line orig_dir proj args =
+  let orig_dir = (* avoids turning foo.v in ./foo.v *)
+    if orig_dir = "." then "" else orig_dir in
+  let error s = Feedback.msg_error (Pp.str (s^".")); exit 1 in
+  let mk_path d =
+    let p = CUnix.correct_path d orig_dir in
+    { path = CUnix.remove_path_dot (post_canonize p);
+      canonical_path = CUnix.canonical_path_name p } in
+  let rec aux proj = function
+  | [] -> proj
+  | "-impredicative-set" :: _ ->
+    error "Use \"-arg -impredicative-set\" instead of \"-impredicative-set\""
+  | "-no-install" :: _ ->
+    error "Use \"-install none\" instead of \"-no-install\""
+  | "-custom" :: _ ->
+    error "Use \"-extra[-phony] target deps command\" instead of \"-custom command deps target\""
+  
+  | ("-no-opt"|"-byte") :: r -> aux { proj with use_ocamlopt =  false } r
+  | ("-full"|"-opt") :: r -> aux { proj with use_ocamlopt =  true } r
+  | "-install" :: d :: r ->
+    if proj.install_kind <> None then
+      Feedback.msg_warning (Pp.str "-install set more than once.");
+    let install = match d with
+      | "user" -> UserInstall
+      | "none" -> NoInstall
+      | "global" -> TraditionalInstall
+      | _ -> error ("invalid option \""^d^"\" passed to -install") in
+    aux { proj with install_kind = Some install } r
+  | "-extra" :: target :: dependencies :: command :: r ->
+    let tgt = { target; dependencies; phony = false; command } in
+    aux { proj with extra_targets = proj.extra_targets @ [tgt] } r
+  | "-extra-phony" :: target :: dependencies :: command :: r ->
+    let tgt = { target; dependencies; phony = true; command } in
+    aux { proj with extra_targets = proj.extra_targets @ [tgt] } r
+
+  | "-Q" :: d :: lp :: r ->
+    aux { proj with q_includes = proj.q_includes @ [mk_path d,lp] } r
+  | "-I" :: d :: r ->
+    aux { proj with ml_includes = proj.ml_includes @ [mk_path d] } r
+  | "-R" :: d :: lp :: r ->
+    aux { proj with r_includes = proj.r_includes @ [mk_path d,lp] } r
+
+  | "-f" :: file :: r ->
+    let file = CUnix.remove_path_dot (CUnix.correct_path file orig_dir) in
+    let () = match proj.project_file with
+      | None -> ()
+      | Some _ -> Feedback.msg_warning (Pp.str
+	"Multiple project files are deprecated.")
+    in
+    let proj = aux { proj with project_file = Some file } (parse file) in
+    aux proj r
+
+  | "-o" :: file :: r ->
+    if String.contains file '/' then
+      error "Output file must be in the current directory";
+    if proj.makefile <> None then
+      error "Option -o given more than once";
+    aux { proj with makefile = Some file } r  
+  | v :: "=" :: def :: r ->
+    aux { proj with defs = proj.defs @ [v,def] } r
+  | "-arg" :: a :: r ->
+    aux { proj with extra_args = proj.extra_args @ [a] } r
+  | f :: r ->
+      let f = CUnix.correct_path f orig_dir in
+      let proj =
+        if is_directory f then { proj with subdirs = proj.subdirs @ [f] }
+        else match CUnix.get_extension f with
+        | ".v" -> { proj with v_files = proj.v_files @ [f] }
+        | ".ml" -> { proj with ml_files = proj.ml_files @ [f] }
+        | ".ml4" -> { proj with ml4_files = proj.ml4_files @ [f] }
+        | ".mli" -> { proj with mli_files = proj.mli_files @ [f] }
+        | ".mllib" -> { proj with mllib_files = proj.mllib_files @ [f] }
+        | ".mlpack" -> { proj with mlpack_files = proj.mlpack_files @ [f] }
+        | _ -> raise (Parsing_error ("Unknown option "^f)) in
+      aux proj r
+ in
+   aux proj args
+
+ (******************************* API ************************************)
+
+let cmdline_args_to_project ~curdir args =
+  process_cmd_line curdir (mk_project None None None true) args
+
+let read_project_file f =
+  process_cmd_line (Filename.dirname f)
+    (mk_project (Some f) None (Some NoInstall) true) (parse f)
+
+let rec find_project_file ~from ~projfile_name =
+  let fname = Filename.concat from projfile_name in
+  if Sys.file_exists fname then Some fname
+  else
+    let newdir = Filename.dirname from in
+    if newdir = "" || newdir = "/" then None
+    else find_project_file ~from:newdir ~projfile_name
+;;
+
+let coqtop_args_from_project
+  { ml_includes; r_includes; q_includes; extra_args }
+=
+  let map = List.map in
+  let args =
+    map (fun { canonical_path = i } -> ["-I"; i]) ml_includes @
+    map (fun ({ canonical_path = i }, l) -> ["-Q"; i; l]) q_includes @
+    map (fun ({ canonical_path = p }, l) -> ["-R"; p; l]) r_includes @
+    [extra_args] in
+  List.flatten args
+;;
+
+(* vim:set ft=ocaml: *)
diff --git a/lib/coqProject_file.mli b/lib/coqProject_file.mli
new file mode 100644
index 000000000..8c8fc068a
--- /dev/null
+++ b/lib/coqProject_file.mli
@@ -0,0 +1,52 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+exception Parsing_error of string
+
+type project = {
+  project_file  : string option;
+  makefile : string option;
+  install_kind  : install option;
+  use_ocamlopt : bool;
+
+  v_files : string list;
+  mli_files : string list;
+  ml4_files : string list;
+  ml_files : string list;
+  mllib_files : string list;
+  mlpack_files : string list;
+
+  ml_includes : path list;
+  r_includes  : (path * logic_path) list;
+  q_includes  : (path * logic_path) list;
+  extra_args : string list;
+  defs : (string * string) list;
+
+  (* deprecated in favor of a Makefile.local using :: rules *)
+  extra_targets : extra_target list;
+  subdirs : string list;
+
+}
+and extra_target = {
+  target : string;
+  dependencies : string;
+  phony : bool;
+  command : string;
+}
+and logic_path = string
+and path = { path : string; canonical_path : string }
+and install =
+  | NoInstall
+  | TraditionalInstall
+  | UserInstall
+
+val cmdline_args_to_project : curdir:string -> string list -> project
+val read_project_file : string -> project
+val coqtop_args_from_project : project -> string list
+val find_project_file : from:string -> projfile_name:string -> string option
+
diff --git a/lib/envars.ml b/lib/envars.ml
index 89ce52831..79516bb1b 100644
--- a/lib/envars.ml
+++ b/lib/envars.ml
@@ -146,12 +146,8 @@ let coqpath =
 
 let exe s = s ^ Coq_config.exec_extension
 
-let guess_ocamlfind () = which (user_path ()) (exe "ocamlfind")
-
 let ocamlfind () =
-  if !Flags.ocamlfind_spec then !Flags.ocamlfind else
-    if !Flags.boot then Coq_config.ocamlfind else
-      try guess_ocamlfind () / "ocamlfind"  with Not_found -> Coq_config.ocamlfind
+  if !Flags.ocamlfind_spec then !Flags.ocamlfind else Coq_config.ocamlfind
 
 (** {2 Camlp4 paths} *)
 
@@ -207,3 +203,28 @@ let xdg_config_dirs warn =
 
 let xdg_dirs ~warn =
   List.filter Sys.file_exists (xdg_data_dirs warn)
+
+(* Print the configuration information *)
+
+let coq_src_subdirs = [ 
+   "config" ; "dev" ; "lib" ; "kernel" ; "library" ;
+   "engine" ; "pretyping" ; "interp" ; "parsing" ; "proofs" ;
+   "tactics" ; "toplevel" ; "printing" ; "intf" ;
+   "grammar" ; "ide" ; "stm"; "vernac" ] @
+   Coq_config.plugins_dirs
+  
+let print_config ?(prefix_var_name="") f =
+  let open Printf in 
+  fprintf f "%sLOCAL=%s\n" prefix_var_name (if Coq_config.local then "1" else "0");
+  fprintf f "%sCOQLIB=%s/\n" prefix_var_name (coqlib ());
+  fprintf f "%sDOCDIR=%s/\n" prefix_var_name (docdir ());
+  fprintf f "%sOCAMLFIND=%s\n" prefix_var_name (ocamlfind ());
+  fprintf f "%sCAMLP4=%s\n" prefix_var_name Coq_config.camlp4;
+  fprintf f "%sCAMLP4O=%s\n" prefix_var_name Coq_config.camlp4o;
+  fprintf f "%sCAMLP4BIN=%s/\n" prefix_var_name (camlp4bin ());
+  fprintf f "%sCAMLP4LIB=%s\n" prefix_var_name (camlp4lib ());
+  fprintf f "%sCAMLP4OPTIONS=%s\n" prefix_var_name Coq_config.camlp4compat;
+  fprintf f "%sHASNATDYNLINK=%s\n" prefix_var_name
+    (if Coq_config.has_natdynlink then "true" else "false");
+  fprintf f "%sCOQ_SRC_SUBDIRS=%s\n" prefix_var_name (String.concat " " coq_src_subdirs)
+
diff --git a/lib/envars.mli b/lib/envars.mli
index 90a42859b..b164e789d 100644
--- a/lib/envars.mli
+++ b/lib/envars.mli
@@ -69,3 +69,9 @@ val xdg_data_home   : (string -> unit) -> string
 val xdg_config_dirs : (string -> unit) -> string list
 val xdg_data_dirs   : (string -> unit) -> string list
 val xdg_dirs : warn : (string -> unit) -> string list
+
+(** {6 Prints the configuration information } *)
+val print_config : ?prefix_var_name:string -> out_channel -> unit
+
+(** Directories in which coq sources are found *)
+val coq_src_subdirs : string list
diff --git a/test-suite/Makefile b/test-suite/Makefile
index afaa48463..c2d6e540c 100644
--- a/test-suite/Makefile
+++ b/test-suite/Makefile
@@ -87,7 +87,7 @@ VSUBSYSTEMS := prerequisite success failure $(BUGS) output \
   output-modulo-time interactive micromega $(COMPLEXITY) modules stm
 
 # All subsystems
-SUBSYSTEMS := $(VSUBSYSTEMS) misc bugs ide vio coqchk
+SUBSYSTEMS := $(VSUBSYSTEMS) misc bugs ide vio coqchk coq-makefile
 
 PREREQUISITELOG = prerequisite/admit.v.log			\
   prerequisite/make_local.v.log prerequisite/make_notation.v.log
@@ -151,6 +151,7 @@ summary:
 	  $(call summary_dir, "IDE tests", ide); \
 	  $(call summary_dir, "VI tests", vio); \
 	  $(call summary_dir, "Coqchk tests", coqchk); \
+	  $(call summary_dir, "Coq makefile", coq-makefile); \
 	  nb_success=`find . -name '*.log' -exec tail -n2 '{}' \; | grep -e $(log_success) | wc -l`; \
 	  nb_failure=`find . -name '*.log' -exec tail -n2 '{}' \; | grep -e $(log_failure) | wc -l`; \
 	  nb_tests=`expr $$nb_success + $$nb_failure`; \
@@ -481,3 +482,19 @@ coqchk: $(patsubst %.v,%.chk.log,$(wildcard coqchk/*.v))
 	    echo "    $<...Error!"; \
 	  fi; \
 	} > "$@"
+
+coq-makefile: $(patsubst %/run.sh,%.log,$(wildcard coq-makefile/*/run.sh))
+
+coq-makefile/%.log : coq-makefile/%/run.sh
+	@echo "TEST      coq-makefile/$*"
+	$(HIDE)(\
+	  cd coq-makefile/$* && \
+	  ./run.sh 2>&1; \
+       	  if [ $$? = 0 ]; then \
+	    echo $(log_success); \
+	    echo "    $<...Ok"; \
+	  else \
+	    echo $(log_failure); \
+	    echo "    $<...Error!"; \
+	  fi; \
+	) > "$@"
diff --git a/test-suite/coq-makefile/arg/_CoqProject b/test-suite/coq-makefile/arg/_CoqProject
new file mode 100644
index 000000000..afdb32e7c
--- /dev/null
+++ b/test-suite/coq-makefile/arg/_CoqProject
@@ -0,0 +1,11 @@
+-R theories test
+-R src test
+-I src
+-arg "-compat 8.4"
+
+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/arg/run.sh b/test-suite/coq-makefile/arg/run.sh
new file mode 100755
index 000000000..28b9bcb96
--- /dev/null
+++ b/test-suite/coq-makefile/arg/run.sh
@@ -0,0 +1,9 @@
+#!/bin/sh
+
+#set -x
+set -e
+
+. ../template/init.sh
+
+coq_makefile -f _CoqProject -o Makefile
+make
diff --git a/test-suite/coq-makefile/compat-subdirs/_CoqProject b/test-suite/coq-makefile/compat-subdirs/_CoqProject
new file mode 100644
index 000000000..4f44bde22
--- /dev/null
+++ b/test-suite/coq-makefile/compat-subdirs/_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
+subdir/
diff --git a/test-suite/coq-makefile/compat-subdirs/run.sh b/test-suite/coq-makefile/compat-subdirs/run.sh
new file mode 100755
index 000000000..ccb348c6f
--- /dev/null
+++ b/test-suite/coq-makefile/compat-subdirs/run.sh
@@ -0,0 +1,9 @@
+#!/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/compat-subdirs/subdir/Makefile b/test-suite/coq-makefile/compat-subdirs/subdir/Makefile
new file mode 100644
index 000000000..846c9b791
--- /dev/null
+++ b/test-suite/coq-makefile/compat-subdirs/subdir/Makefile
@@ -0,0 +1,3 @@
+all:
+	test -f ../theories/test.vo
+	touch done
diff --git a/test-suite/coq-makefile/coqdoc1/_CoqProject b/test-suite/coq-makefile/coqdoc1/_CoqProject
new file mode 100644
index 000000000..35792066b
--- /dev/null
+++ b/test-suite/coq-makefile/coqdoc1/_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/coqdoc1/run.sh b/test-suite/coq-makefile/coqdoc1/run.sh
new file mode 100755
index 000000000..e071f1db7
--- /dev/null
+++ b/test-suite/coq-makefile/coqdoc1/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/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
new file mode 100644
index 000000000..69f47302e
--- /dev/null
+++ b/test-suite/coq-makefile/merlin1/_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/merlin1/run.sh b/test-suite/coq-makefile/merlin1/run.sh
new file mode 100755
index 000000000..9b89e5b6e
--- /dev/null
+++ b/test-suite/coq-makefile/merlin1/run.sh
@@ -0,0 +1,15 @@
+#!/bin/sh
+
+#set -x
+set -e
+
+. ../template/init.sh
+
+coq_makefile -f _CoqProject -o Makefile
+make .merlin
+cat > desired <<EOT
+B src
+S src
+EOT
+tail -2 .merlin > actual
+exec diff -u desired actual
diff --git a/test-suite/coq-makefile/mlpack1/_CoqProject b/test-suite/coq-makefile/mlpack1/_CoqProject
new file mode 100644
index 000000000..69f47302e
--- /dev/null
+++ b/test-suite/coq-makefile/mlpack1/_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/mlpack1/run.sh b/test-suite/coq-makefile/mlpack1/run.sh
new file mode 100755
index 000000000..418a2fb77
--- /dev/null
+++ b/test-suite/coq-makefile/mlpack1/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/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/only/_CoqProject b/test-suite/coq-makefile/only/_CoqProject
new file mode 100644
index 000000000..357384fdd
--- /dev/null
+++ b/test-suite/coq-makefile/only/_CoqProject
@@ -0,0 +1,11 @@
+-R theories/ test
+-R src/ 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/only/run.sh b/test-suite/coq-makefile/only/run.sh
new file mode 100755
index 000000000..4b471bcb8
--- /dev/null
+++ b/test-suite/coq-makefile/only/run.sh
@@ -0,0 +1,12 @@
+#!/bin/sh
+
+#set -x
+set -e
+
+. ../template/init.sh
+
+coq_makefile -f _CoqProject -o Makefile
+make only TGTS="src/test.cmi src/test_aux.cmi" -j2
+test -f src/test.cmi
+test -f src/test_aux.cmi
+! test -f src/test.cmo
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
--- /dev/null
+++ b/test-suite/coq-makefile/template/src/test.mli
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
new file mode 100644
index 000000000..35792066b
--- /dev/null
+++ b/test-suite/coq-makefile/uninstall1/_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/uninstall1/run.sh b/test-suite/coq-makefile/uninstall1/run.sh
new file mode 100755
index 000000000..d24176279
--- /dev/null
+++ b/test-suite/coq-makefile/uninstall1/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/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
diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in
new file mode 100644
index 000000000..5231899c6
--- /dev/null
+++ b/tools/CoqMakefile.in
@@ -0,0 +1,627 @@
+###############################################################################
+##  v      #                   The Coq Proof Assistant                       ##
+## <O___,, #                INRIA - CNRS - LIX - LRI - PPS                   ##
+##   \VV/  #                                                                 ##
+##    //   #                                                                 ##
+###############################################################################
+## GNUMakefile for Coq @COQ_VERSION@
+  
+# For debugging purposes (must stay here, don't move below)
+INITIAL_VARS := $(.VARIABLES)
+# To implement recursion we save the name of the main Makefile
+SELF := $(lastword $(MAKEFILE_LIST))
+
+# This file is generated by coq_makefile and contains many variable
+# definitions, like the list of .v files or the path to Coq
+include @CONF_FILE@
+
+# Put in place old names
+VFILES            := $(COQMF_VFILES)
+MLIFILES          := $(COQMF_MLIFILES)
+MLFILES           := $(COQMF_MLFILES)
+ML4FILES          := $(COQMF_ML4FILES)
+MLPACKFILES       := $(COQMF_MLPACKFILES)
+MLLIBFILES        := $(COQMF_MLLIBFILES)
+INSTALLCOQDOCROOT := $(COQMF_INSTALLCOQDOCROOT)
+OTHERFLAGS        := $(COQMF_OTHERFLAGS)
+COQ_SRC_SUBDIRS   := $(COQMF_COQ_SRC_SUBDIRS)
+OCAMLLIBS         := $(COQMF_OCAMLLIBS)
+SRC_SUBDIRS       := $(COQMF_SRC_SUBDIRS)
+COQLIBS           := $(COQMF_COQLIBS)
+COQLIBS_NOML      := $(COQMF_COQLIBS_NOML)
+LOCAL             := $(COQMF_LOCAL)
+COQLIB            := $(COQMF_COQLIB)
+DOCDIR            := $(COQMF_DOCDIR)
+OCAMLFIND         := $(COQMF_OCAMLFIND)
+CAMLP4            := $(COQMF_CAMLP4)
+CAMLP4O           := $(COQMF_CAMLP4O)
+CAMLP4BIN         := $(COQMF_CAMLP4BIN)
+CAMLP4LIB         := $(COQMF_CAMLP4LIB)
+CAMLP4OPTIONS     := $(COQMF_CAMLP4OPTIONS)
+HASNATDYNLINK     := $(COQMF_HASNATDYNLINK)
+COQ_SRC_SUBDIRS   := $(COQMF_COQ_SRC_SUBDIRS)
+
+@CONF_FILE@: @PROJECT_FILE@
+	@COQ_MAKEFILE_INVOCATION@
+
+# This file can be created by the user to hook into double colon rules or
+# add any other Makefile code he may need
+-include @LOCAL_FILE@
+
+# Parameters ##################################################################
+#
+# Parameters are make variable assignments.
+# They can be passed to (each call to) make on the command line.
+# They can also be put in @LOCAL_FILE@ once an forall.
+# For retro-compatibility reasons they can be put in the _CoqProject, but this
+# practice is discouraged since _CoqProject better not contain make specific
+# code (be nice to user interfaces).
+
+# Print shell commands (set to non empty)
+VERBOSE ?=
+
+# Time the Coq process (set to non empty), and how (see default value)
+TIMED?=
+TIMECMD?=
+STDTIME?=/usr/bin/time -f "$* (user: %U mem: %M ko)"
+
+# Coq binaries
+COQC     ?= $(TIMER) "$(COQBIN)coqc"
+COQCHK   ?= $(TIMER) "$(COQBIN)coqchk"
+COQDEP   ?= "$(COQBIN)coqdep"
+GALLINA  ?= "$(COQBIN)gallina"
+COQDOC   ?= "$(COQBIN)coqdoc"
+COQMKTOP ?= "$(COQBIN)coqmktop"
+
+# OCaml binaries
+CAMLC       ?= $(OCAMLFIND) ocamlc -c -rectypes -thread
+CAMLOPTC    ?= $(OCAMLFIND) opt    -c -rectypes -thread
+CAMLLINK    ?= $(OCAMLFIND) ocamlc    -rectypes -thread
+CAMLOPTLINK ?= $(OCAMLFIND) opt       -rectypes -thread
+CAMLDEP     ?= $(OCAMLFIND) ocamldep -slash -ml-synonym .ml4 -ml-synonym .mlpack
+
+# DESTDIR is prepended to all installation paths
+DESTDIR ?= 
+
+# Debug builds, typically -g to OCaml, -debug to Coq.
+CAMLDEBUG ?=
+COQDEBUG ?=
+
+
+
+########## End of parameters ##################################################
+# What follows may be relevant to you only if you need to
+# extend this Makefile.  If so, look for 'Extension point' here and
+# put in @LOCAL_FILE@ double colon rules accordingly.
+# E.g. to perform some work after the all target completes you can write
+#
+# post-all::
+# 	echo "All done!"
+# 
+# in @LOCAL_FILE@
+#
+###############################################################################
+
+
+
+
+# Flags #######################################################################
+#
+# We define a bunch of variables combining the parameters 
+
+SHOW := $(if $(VERBOSE),@true "",@echo "")
+HIDE := $(if $(VERBOSE),,@)
+
+TIMER=$(if $(TIMED), $(STDTIME), $(TIMECMD))
+
+OPT?=
+
+COQFLAGS?=-q $(OPT) $(COQLIBS) $(OTHERFLAGS)
+COQCHKFLAGS?=-silent -o $(COQLIBS) 
+COQDOCFLAGS?=-interpolate -utf8 $(COQLIBS_NOML)
+
+# The version of Coq being run and the version of coq_makefile that
+# generated this makefile
+COQ_VERSION:=$(shell $(COQC) --print-version | cut -d ' ' -f 1)
+COQMAKEFILE_VERSION:=@COQ_VERSION@
+
+COQSRCLIBS?= $(foreach d,$(COQ_SRC_SUBDIRS), -I "$(COQLIB)$(d)")
+
+CAMLFLAGS=$(OCAMLLIBS) $(COQSRCLIBS) -I $(CAMLP4LIB)
+
+CAMLLIB:=$(shell $(OCAMLFIND) printconf stdlib)
+
+# FIXME This should be generated by Coq
+GRAMMARS:=grammar.cma
+ifeq ($(CAMLP4),camlp5)
+CAMLP4EXTEND=pa_extend.cmo q_MLast.cmo pa_macro.cmo
+else
+CAMLP4EXTEND=
+endif
+
+PP:=-pp '$(CAMLP4O) -I $(CAMLLIB) -I $(COQLIB)/grammar compat5.cmo $(CAMLP4EXTEND) $(GRAMMARS) $(CAMLP4OPTIONS) -impl'
+
+COQLIBINSTALL = $(COQLIB)user-contrib
+COQDOCINSTALL = $(DOCDIR)user-contrib
+COQTOPINSTALL = $(COQLIB)toploop
+
+# Retro compatibility (DESTDIR is standard on Unix, DESTROOT is not) 
+ifneq "$(DSTROOT)" ""
+DESTDIR := $(DSTROOT)
+endif
+
+# Files #######################################################################
+#
+# We here define a bunch of variables about the files being part of the
+# Coq project in order to ease the writing of build target and build rules
+
+ALLSRCFILES := \
+	$(VFILES) \
+	$(ML4FILES) \
+	$(MLFILES) \
+	$(MLPACKFILES) \
+	$(MLLIBFILES) \
+	$(MLIFILES)
+
+# helpers
+vo_to_obj = $(addsuffix .o,\
+  $(filter-out Warning: Error:,\
+  $(shell $(COQBIN)coqtop -q -noinit -batch -quiet -print-mod-uid $(1))))
+strip_dotslash = $(patsubst ./%,%,$(1))
+VO = vo
+
+VOFILES = $(VFILES:.v=.$(VO))
+GLOBFILES = $(VFILES:.v=.glob)
+GFILES = $(VFILES:.v=.g)
+HTMLFILES = $(VFILES:.v=.html)
+GHTMLFILES = $(VFILES:.v=.g.html)
+BEAUTYFILES = $(addsuffix .beautified,$(VFILES))
+TEXFILES = $(VFILES:.v=.tex)
+GTEXFILES = $(VFILES:.v=.g.tex)
+CMOFILES = \
+	$(ML4FILES:.ml4=.cmo) \
+	$(MLFILES:.ml=.cmo) \
+	$(MLPACKFILES:.mlpack=.cmo)
+CMXFILES = $(CMOFILES:.cmo=.cmx)
+OFILES = $(CMXFILES:.cmx=.o)
+CMAFILES = $(MLLIBFILES:.mllib=.cma)
+CMXAFILES = $(CMAFILES:.cma=.cmxa)
+CMIFILES = \
+	$(CMOFILES:.cmo=.cmi) \
+	$(MLIFILES:.mli=.cmi)
+# the /if/ is because old _CoqProject did not list a .ml(pack|lib) but just
+# a .ml4 file
+CMXSFILES = \
+	$(MLPACKFILES:.mlpack=.cmxs) \
+	$(CMXAFILES:.cmxa=.cmxs) \
+	$(if $(MLPACKFILES)$(CMXAFILES),,\
+		$(ML4FILES:.ml4=.cmxs) $(MLFILES:.ml=.cmxs))
+
+# files that are packed into a plugin (no extension)
+PACKEDFILES = \
+	$(call strip_dotslash, \
+	  $(foreach lib, \
+            $(call strip_dotslash, \
+	       $(MLPACKFILES:.mlpack=_MLPACK_DEPENDENCIES)),$($(lib))))
+# files that are archived into a .cma (mllib)
+LIBEDFILES = \
+	$(call strip_dotslash, \
+	  $(foreach lib, \
+            $(call strip_dotslash, \
+	       $(MLLIBFILES:.mllib=_MLLIB_DEPENDENCIES)),$($(lib))))
+CMIFILESTOINSTALL = $(filter-out $(addsuffix .cmi,$(PACKEDFILES)),$(CMIFILES))
+CMOFILESTOINSTALL = $(filter-out $(addsuffix .cmo,$(PACKEDFILES)),$(CMOFILES))
+OBJFILES = $(call vo_to_obj,$(VOFILES))
+ALLNATIVEFILES = \
+	$(OBJFILES:.o=.cmi) \
+	$(OBJFILES:.o=.cmo) \
+	$(OBJFILES:.o=.cmx) \
+	$(OBJFILES:.o=.cmxs)
+# trick: wildcard filters out non-existing files
+NATIVEFILESTOINSTALL = $(foreach f, $(ALLNATIVEFILES), $(wildcard $f))
+FILESTOINSTALL = \
+	$(VOFILES) \
+	$(VFILES) \
+	$(GLOBFILES) \
+	$(NATIVEFILESTOINSTALL) \
+	$(CMOFILESTOINSTALL) \
+	$(CMIFILESTOINSTALL) \
+	$(CMAFILES)
+ifeq '$(HASNATDYNLINK)' 'true'
+DO_NATDYNLINK = yes
+FILESTOINSTALL += $(CMXSFILES) $(CMXAFILES) $(CMOFILESTOINSTALL:.cmo=.cmx)
+else
+DO_NATDYNLINK =
+endif
+
+ALLDFILES = $(addsuffix .d,$(ALLSRCFILES))
+
+# Compilation targets #########################################################
+
+all: 
+	$(HIDE)$(MAKE) --no-print-directory -f "$(SELF)" pre-all
+	$(HIDE)$(MAKE) --no-print-directory -f "$(SELF)" real-all
+	$(HIDE)$(MAKE) --no-print-directory -f "$(SELF)" post-all
+.PHONY: all
+
+# Extension points for actions to be performed before/after the all target
+pre-all::
+	@# Extension point
+	$(HIDE)if [ "$(COQMAKEFILE_VERSION)" != "$(COQ_VERSION)" ]; then\
+	  echo "W: This Makefile was generated by Coq $(COQMAKEFILE_VERSION)";\
+	  echo "W: while the current Coq version is $(COQ_VERSION)";\
+	fi
+.PHONY: pre-all
+
+post-all::
+	@# Extension point
+.PHONY: post-all
+
+real-all: $(VOFILES) $(CMOFILES) $(CMAFILES) $(if $(DO_NATDYNLINK),$(CMXSFILES))
+.PHONY: real-all
+
+# FIXME, see Ralph's bugreport
+quick: $(VOFILES:.vo=.vio)
+.PHONY: quick
+
+vio2vo:
+	$(COQC) $(COQDEBUG) $(COQFLAGS) \
+		-schedule-vio2vo $(J) $(VOFILES:%.vo=%.vio)
+.PHONY: vio2vo
+
+checkproofs:
+	$(COQC) $(COQDEBUG) $(COQFLAGS) \
+		-schedule-vio-checking $(J) $(VOFILES:%.vo=%.vio)
+.PHONY: checkproofs
+
+validate: $(VOFILES)
+	$(COQCHK) $(COQCHKFLAGS) $(notdir $(^:.vo=))
+.PHONY: validate
+
+only: $(TGTS)
+.PHONY: only
+
+# Documentation targets #######################################################
+
+html: $(GLOBFILES) $(VFILES)
+	$(SHOW)'COQDOC -d html $(GAL)'
+	$(HIDE)mkdir -p html
+	$(HIDE)$(COQDOC) \
+		-toc $(COQDOCFLAGS) -html $(GAL) $(COQDOCLIBS) -d html $(VFILES)
+
+mlihtml: $(MLIFILES:.mli=.cmi)
+	$(SHOW)'OCAMLDOC -d $@'
+	$(HIDE)mkdir $@ || rm -rf $@/*
+	$(HIDE)$(OCAMLFIND) ocamldoc -html -rectypes \
+		-d $@ -m A $(CAMLDEBUG) $(CAMLFLAGS) $(MLIFILES)
+
+all-mli.tex: $(MLIFILES:.mli=.cmi)
+	$(SHOW)'OCAMLDOC -latex $@'
+	$(OCAMLFIND) ocamldoc -latex -rectypes \
+		-o $@ -m A $(CAMLDEBUG) $(CAMLFLAGS) $(MLIFILES)
+
+gallina: $(GFILES)
+
+all.ps: $(VFILES)
+	$(SHOW)'COQDOC -ps $(GAL)'
+	$(HIDE)$(COQDOC) \
+		-toc $(COQDOCFLAGS) -ps $(GAL) $(COQDOCLIBS) \
+		-o $@ `$(COQDEP) -sort -suffix .v $(VFILES)`
+
+all.pdf: $(VFILES)
+	$(SHOW)'COQDOC -pdf $(GAL)'
+	$(HIDE)$(COQDOC) \
+		-toc $(COQDOCFLAGS) -pdf $(GAL) $(COQDOCLIBS) \
+		-o $@ `$(COQDEP) -sort -suffix .v $(VFILES)`
+
+# FIXME: not quite right, since the output name is different
+gallinahtml: GAL=g
+gallinahtml: html
+
+all-gal.ps: GAL=-g
+all-gal.ps: all.ps
+
+all-gal.pdf: GAL=-g
+all-gal.pdf: all.pdf
+
+# ?
+beautify: $(BEAUTYFILES)
+	for file in $^; do mv $${file%.beautified} $${file%beautified}old && mv $${file} $${file%.beautified}; done
+	@echo 'Do not do "make clean" until you are sure that everything went well!'
+	@echo 'If there were a problem, execute "for file in $$(find . -name \*.v.old -print); do mv $${file} $${file%.old}; done" in your shell/'
+.PHONY: beautify
+
+# Installation targets ########################################################
+#
+# There rules can be extended in @LOCAL_FILE@
+# Extensions can't assume when they run.
+
+install: install-extra
+	$(HIDE)for f in $(FILESTOINSTALL); do\
+	 df="`$(COQMF_MAKEFILE) -destination-of "$$f" $(COQLIBS)`";\
+	 if [ -z "$$df" ]; then\
+	   echo SKIP "$$f" since it has no logical path;\
+	 else\
+	   install -d "$(DESTDIR)$(COQLIBINSTALL)/$$df"; \
+	   install -m 0644 "$$f" "$(DESTDIR)$(COQLIBINSTALL)/$$df"; \
+	   echo INSTALL "$$f" "$(DESTDIR)$(COQLIBINSTALL)/$$df";\
+	 fi;\
+	done
+install-extra::
+	@# Extension point
+.PHONY: install install-extra
+
+install-doc:: html mlihtml
+	@# Extension point
+	$(HIDE)install -d "$(DESTDIR)$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/html"
+	$(HIDE)for i in html/*; do \
+	 dest="$(DESTDIR)$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/$$i";\
+	 install -m 0644 "$$i" "$$dest";\
+	 echo INSTALL "$$i" "$$dest";\
+	done
+	$(HIDE)install -d \
+		"$(DESTDIR)$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/mlihtml"
+	$(HIDE)for i in mlihtml/*; do \
+	 dest="$(DESTDIR)$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/$$i";\
+	 install -m 0644 "$$i" "$$dest";\
+	 echo INSTALL "$$i" "$$dest";\
+	done
+.PHONY: install-doc
+
+uninstall::
+	@# Extension point
+	$(HIDE)for f in $(FILESTOINSTALL); do \
+	 df="`$(COQMF_MAKEFILE) -destination-of "$$f" $(COQLIBS)`";\
+	 instf="$(DESTDIR)$(COQLIBINSTALL)/$$df/`basename $$f`"; \
+	 rm -f "$$instf";\
+	 echo RM "$$instf"; \
+	 rmdir --ignore-fail-on-non-empty "$(DESTDIR)$(COQLIBINSTALL)/$$df/"; \
+	done
+.PHONY: uninstall
+
+uninstall-doc::
+	@# Extension point
+	$(SHOW)'RM $(DESTDIR)$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/html'
+	$(HIDE)rm -rf "$(DESTDIR)$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/html"
+	$(SHOW)'RM $(DESTDIR)$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/mlihtml'
+	$(HIDE)rm -rf "$(DESTDIR)$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/mlihtml"
+	$(HIDE)rmdir --ignore-fail-on-non-empty \
+		"$(DESTDIR)$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/"
+.PHONY: uninstall-doc
+
+# Cleaning ####################################################################
+#
+# There rules can be extended in @LOCAL_FILE@
+# Extensions can't assume when they run.
+
+clean::
+	@# Extension point
+	$(SHOW)'CLEAN'
+	$(HIDE)rm -f $(CMOFILES)
+	$(HIDE)rm -f $(CMIFILES)
+	$(HIDE)rm -f $(CMAFILES)
+	$(HIDE)rm -f $(CMOFILES:.cmo=.cmx) 
+	$(HIDE)rm -f $(CMXAFILES)
+	$(HIDE)rm -f $(CMXSFILES) 
+	$(HIDE)rm -f $(CMOFILES:.cmo=.o) 
+	$(HIDE)rm -f $(CMXAFILES:.cmxa=.a)
+	$(HIDE)rm -f $(ALLDFILES)
+	$(HIDE)rm -f $(ALLNATIVEFILES)
+	$(HIDE)find . -name .coq-native -type d -empty -delete
+	$(HIDE)rm -f $(VOFILES)
+	$(HIDE)rm -f $(VOFILES:.vo=.vio)
+	$(HIDE)rm -f $(GFILES)
+	$(HIDE)rm -f $(BEAUTYFILES) $(VFILES:=.old)
+	$(HIDE)rm -f all.ps all-gal.ps all.pdf all-gal.pdf all.glob all-mli.tex
+	$(HIDE)rm -f $(VFILES:.v=.glob)
+	$(HIDE)rm -f $(VFILES:.v=.tex)
+	$(HIDE)rm -f $(VFILES:.v=.g.tex)
+	$(HIDE)rm -rf html mlihtml
+.PHONY: clean
+
+cleanall:: clean
+	@# Extension point
+	$(SHOW)'CLEAN *.aux'
+	$(HIDE)rm -f $(foreach f,$(VFILES:.v=),$(dir $(f)).$(notdir $(f)).aux)
+.PHONY: cleanall
+
+archclean::
+	@# Extension point
+	$(SHOW)'CLEAN *.cmx *.o'
+	$(HIDE)rm -f $(ALLNATIVEFILES)
+	$(HIDE)rm -f $(CMOFILES:%.cmo=%.cmx)
+.PHONY: archclean
+
+
+# Compilation rules ###########################################################
+
+$(MLIFILES:.mli=.cmi): %.cmi: %.mli
+	$(SHOW)'CAMLC -c $<'
+	$(HIDE)$(CAMLC) $(CAMLDEBUG) $(CAMLFLAGS) $<
+
+$(ML4FILES:.ml4=.cmo): %.cmo: %.ml4
+	$(SHOW)'CAMLC -pp -c $<'
+	$(HIDE)$(CAMLC) $(CAMLDEBUG) $(CAMLFLAGS) $(PP) -impl $<
+
+$(ML4FILES:.ml4=.cmx): %.cmx: %.ml4
+	$(SHOW)'CAMLOPT -pp -c $(FOR_PACK) $<'
+	$(HIDE)$(CAMLOPTC) $(CAMLDEBUG) $(CAMLFLAGS) $(PP) $(FOR_PACK) -impl $<
+
+$(MLFILES:.ml=.cmo): %.cmo: %.ml
+	$(SHOW)'CAMLC -c $<'
+	$(HIDE)$(CAMLC) $(CAMLDEBUG) $(CAMLFLAGS) $<
+
+$(MLFILES:.ml=.cmx): %.cmx: %.ml
+	$(SHOW)'CAMLOPT -c $(FOR_PACK) $<'
+	$(HIDE)$(CAMLOPTC) $(CAMLDEBUG) $(CAMLFLAGS) $(FOR_PACK) $<
+
+
+$(MLLIBFILES:.mllib=.cmxs): %.cmxs: %.cmxa
+	$(SHOW)'CAMLOPT -shared -o $@'
+	$(HIDE)$(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) \
+		-linkall -shared -o $@ $<
+
+$(MLLIBFILES:.mllib=.cma): %.cma: | %.mllib
+	$(SHOW)'CAMLC -a -o $@'
+	$(HIDE)$(CAMLLINK) $(CAMLDEBUG) $(CAMLFLAGS) -a -o $@ $^
+
+$(MLLIBFILES:.mllib=.cmxa): %.cmxa: | %.mllib
+	$(SHOW)'CAMLOPT -a -o $@'
+	$(HIDE)$(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) -a -o $@ $^
+
+
+$(MLPACKFILES:.mlpack=.cmxs): %.cmxs: %.cmx
+	$(SHOW)'CAMLOPT -shared -o $@'
+	$(HIDE)$(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) -shared -o $@ $<
+
+$(MLPACKFILES:.mlpack=.cmo): %.cmo: | %.mlpack
+	$(SHOW)'CAMLC -pack -o $@'
+	$(HIDE)$(CAMLLINK) $(CAMLDEBUG) $(CAMLFLAGS) -pack -o $@ $^
+
+$(MLPACKFILES:.mlpack=.cmx): %.cmx: | %.mlpack
+	$(SHOW)'CAMLOPT -pack -o $@'
+	$(HIDE)$(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) -pack -o $@ $^
+
+# This rule is for _CoqProject with no .mllib nor .mlpack 
+$(filter-out $(MLLIBFILES:.mllib=.cmxs) $(MLPACKFILES:.mlpack=.cmxs) $(addsuffix .cmxs,$(PACKEDFILES)) $(addsuffix .cmxs,$(LIBEDFILES)),$(MLFILES:.ml=.cmxs) $(ML4FILES:.ml4=.cmxs)): %.cmxs: %.cmx
+	$(SHOW)'[deprecated,use-mllib-or-mlpack] CAMLOPT -shared -o $@'
+	$(HIDE)$(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) -shared -o $@ $<
+
+$(VOFILES): %.vo: %.v
+	$(SHOW)COQC $<
+	$(HIDE)$(COQC) $(COQDEBUG) $(COQFLAGS) $<
+
+# FIXME ?merge with .vo / .vio ?
+$(GLOBFILES): %.glob: %.v
+	$(COQC) $(COQDEBUG) $(COQFLAGS) $<
+
+$(VFILES:.v=.vio): %.vio: %.v
+	$(SHOW)COQC -quick $<
+	$(HIDE)$(COQC) -quick $(COQDEBUG) $(COQFLAGS) $<
+
+$(BEAUTYFILES): %.v.beautified: %.v
+	$(SHOW)'BEAUTIFY $<'
+	$(HIDE)$(COQC) $(COQDEBUG) $(COQFLAGS) -beautify $<
+
+$(GFILES): %.g: %.v
+	$(SHOW)'GALLINA $<'
+	$(HIDE)$(GALLINA) $<
+
+$(TEXFILES): %.tex: %.v
+	$(SHOW)'COQDOC -latex $<'
+	$(HIDE)$(COQDOC) $(COQDOCFLAGS) -latex $< -o $@
+
+$(GTEXFILES): %.g.tex: %.v
+	$(SHOW)'COQDOC -latex -g $<'
+	$(HIDE)$(COQDOC) $(COQDOCFLAGS) -latex -g $< -o $@
+
+$(HTMLFILES): %.html: %.v %.glob
+	$(SHOW)'COQDOC -html $<'
+	$(HIDE)$(COQDOC) $(COQDOCFLAGS) -html $< -o $@
+
+$(GHTMLFILES): %.g.html: %.v %.glob
+	$(SHOW)'COQDOC -html -g $<'
+	$(HIDE)$(COQDOC) $(COQDOCFLAGS)  -html -g $< -o $@
+
+# Dependency files ############################################################
+
+ifneq ($(filter-out archclean clean cleanall printenv,$(MAKECMDGOALS)),)
+ -include $(ALLDFILES)
+else
+ ifeq ($(MAKECMDGOALS),)
+  -include $(ALLDFILES)
+ endif
+endif
+
+.SECONDARY: $(ALLDFILES)
+
+redir_if_ok = > "$@" || ( RV=$$?; rm -f "$@"; exit $$RV )
+
+$(addsuffix .d,$(MLIFILES)): %.mli.d: %.mli
+	$(SHOW)'CAMLDEP $<'
+	$(HIDE)$(CAMLDEP) $(OCAMLLIBS) "$<" $(redir_if_ok)
+
+$(addsuffix .d,$(ML4FILES)): %.ml4.d: %.ml4
+	$(SHOW)'CAMLDEP -pp $<'
+	$(HIDE)$(CAMLDEP) $(OCAMLLIBS) $(PP) -impl "$<" $(redir_if_ok)
+
+$(addsuffix .d,$(MLFILES)): %.ml.d: %.ml
+	$(SHOW)'CAMLDEP $<'
+	$(HIDE)$(CAMLDEP) $(OCAMLLIBS) "$<" $(redir_if_ok)
+
+$(addsuffix .d,$(MLLIBFILES)): %.mllib.d: %.mllib
+	$(SHOW)'COQDEP $<'
+	$(HIDE)$(COQDEP) $(OCAMLLIBS) -c "$<" $(redir_if_ok)
+
+$(addsuffix .d,$(MLPACKFILES)): %.mlpack.d: %.mlpack
+	$(SHOW)'COQDEP $<'
+	$(HIDE)$(COQDEP) $(OCAMLLIBS) -c "$<" $(redir_if_ok)
+
+$(addsuffix .d,$(VFILES)): %.v.d: %.v
+	$(SHOW)'COQDEP $<'
+	$(HIDE)$(COQDEP) $(COQLIBS) -c "$<" $(redir_if_ok)
+
+# Misc ########################################################################
+
+byte:
+	$(HIDE)$(MAKE) all "OPT:=-byte" -f "$(SELF)"
+.PHONY: byte
+
+opt:
+	$(HIDE)$(MAKE) all "OPT:=-opt" -f "$(SELF)"
+.PHONY:	opt 
+
+# This is deprecated.  To extend this makefile use
+# extension points and @LOCAL_FILE@
+printenv::
+	$(warning printenv is deprecated)
+	$(warning write extensions in @LOCAL_FILE@ or include @CONF_FILE@)
+	@echo 'LOCAL = $(LOCAL)'
+	@echo 'COQLIB = $(COQLIB)'
+	@echo 'DOCDIR = $(DOCDIR)'
+	@echo 'OCAMLFIND = $(OCAMLFIND)'
+	@echo 'CAMLP4 = $(CAMLP4)'
+	@echo 'CAMLP4O = $(CAMLP4O)'
+	@echo 'CAMLP4BIN = $(CAMLP4BIN)'
+	@echo 'CAMLP4LIB = $(CAMLP4LIB)'
+	@echo 'CAMLP4OPTIONS = $(CAMLP4OPTIONS)'
+	@echo 'HASNATDYNLINK = $(HASNATDYNLINK)'
+	@echo 'SRC_SUBDIRS = $(SRC_SUBDIRS)'
+	@echo 'COQ_SRC_SUBDIRS = $(COQ_SRC_SUBDIRS)'
+	@echo 'OCAMLFIND = $(OCAMLFIND)'
+	@echo 'PP = $(PP)'
+	@echo 'COQFLAGS = $(COQFLAGS)'
+	@echo 'COQLIBINSTALL = $(COQLIBINSTALL)'
+	@echo 'COQDOCINSTALL = $(COQDOCINSTALL)'
+.PHONY:	printenv
+
+# Generate a .merlin file.  If you need to append directives to this
+# file you can extend the merlin-hook target in @LOCAL_FILE@
+.merlin:
+	$(SHOW)'FILL .merlin'
+	$(HIDE)echo 'FLG -rectypes' > .merlin
+	$(HIDE)echo "B $(COQLIB)" >> .merlin
+	$(HIDE)echo "S $(COQLIB)" >> .merlin
+	$(HIDE)$(foreach d,$(COQ_SRC_SUBDIRS), \
+		echo "B $(COQLIB)$(d)" >> .merlin;)
+	$(HIDE)$(foreach d,$(COQ_SRC_SUBDIRS), \
+		echo "S $(COQLIB)$(d)" >> .merlin;)
+	$(HIDE)$(foreach d,$(SRC_SUBDIRS), echo "B $(d)" >> .merlin;)
+	$(HIDE)$(foreach d,$(SRC_SUBDIRS), echo "S $(d)" >> .merlin;)
+	$(HIDE)$(MAKE) merlin-hook -f "$(SELF)"
+.PHONY: merlin
+
+merlin-hook::
+	@# Extension point
+.PHONY: merlin-hook
+
+# prints all variables
+debug:
+	$(foreach v,\
+		$(sort $(filter-out $(INITIAL_VARS) INITIAL_VARS,\
+	       		$(.VARIABLES))),\
+	       	$(info $(v) = $($(v))))
+.PHONY: debug
+
+.DEFAULT_GOAL := all
+
diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml
index 4875cb62b..78c92e68b 100644
--- a/tools/coq_makefile.ml
+++ b/tools/coq_makefile.ml
@@ -8,17 +8,13 @@
 
 (* Coq_makefile: automatically create a Makefile for a Coq development *)
 
+open CoqProject_file
+open Printf
+
 let output_channel = ref stdout
 let makefile_name = ref "Makefile"
 let make_name = ref ""
 
-let some_vfile = ref false
-let some_mlfile = ref false
-let some_mlifile = ref false
-let some_ml4file = ref false
-let some_mllibfile = ref false
-let some_mlpackfile = ref false
-
 let print x = output_string !output_channel x
 let printf x = Printf.fprintf !output_channel x
 
@@ -31,29 +27,10 @@ let rec print_prefix_list sep = function
   | x :: l -> print sep; print x; print_prefix_list sep l
   | [] -> ()
 
-let section s =
-  let l = String.length s in
-  let print_com s =
-    print "#";
-    print s;
-    print "#\n" in
-  print_com (String.make (l+2) '#');
-  print_com (String.make (l+2) ' ');
-  print "# "; print s; print " #\n";
-  print_com (String.make (l+2) ' ');
-  print_com (String.make (l+2) '#');
-  print "\n"
-
 (* These are the Coq library directories that are used for
  * plugin development
  *)
-let lib_dirs =
-  ["kernel"; "lib"; "library"; "parsing";
-   "pretyping"; "interp"; "printing"; "intf";
-   "proofs"; "tactics"; "tools";
-   "vernac"; "stm"; "toplevel"; "grammar"; "config";
-   "engine"]
-
+let lib_dirs = Envars.coq_src_subdirs
 
 let usage () =
   output_string stderr "Usage summary:\
@@ -104,12 +81,6 @@ let is_genrule r = (* generic rule (like bar%foo: ...) *)
     let genrule = Str.regexp("%") in
       Str.string_match genrule r 0
 
-let string_prefix a b =
-  let rec aux i =
-    try if a.[i] = b.[i] then aux (i+1) else i with Invalid_argument _ -> i
-  in
-  String.sub a 0 (aux 0)
-
 let is_prefix dir1 dir2 =
   let l1 = String.length dir1 in
   let l2 = String.length dir2 in
@@ -122,830 +93,341 @@ let is_prefix dir1 dir2 =
   else false
 
 let physical_dir_of_logical_dir ldir =
-  let le = String.length ldir - 1 in
+  let ldir = Bytes.of_string ldir in
+  let le = Bytes.length ldir - 1 in
   let pdir =
-    if le >= 0 && ldir.[le] = '.' then String.sub ldir 0 (le - 1)
-    else ldir
-  in
-  String.map (fun c -> if c = '.' then '/' else c) pdir
-
-let standard opt =
-  print "byte:\n";
-  print "\t$(MAKE) all \"OPT:=-byte\"\n\n";
-  print "opt:\n";
-  if not opt then print "\t@echo \"WARNING: opt is disabled\"\n";
-  print "\t$(MAKE) all \"OPT:="; print (if opt then "-opt" else "-byte");
-  print "\"\n\n"
-
-let classify_files_by_root var files (inc_ml,inc_i,inc_r) =
-  if List.exists (fun (pdir,_,_) -> pdir = ".") inc_r ||
-     List.exists (fun (pdir,_,_) -> pdir = ".") inc_i
-  then ()
-  else
-    let absdir_of_files =List.rev_map
-	(fun x -> CUnix.canonical_path_name (Filename.dirname x))
-	files
-    in
-    (* files in scope of a -I option (assuming they are no overlapping) *)
-    if List.exists (fun (_,a) -> List.mem a absdir_of_files) inc_ml then
-      begin
-	printf "%sINC=" var;
-	List.iter (fun (pdir,absdir) ->
-		   if List.mem absdir absdir_of_files
-		   then printf "$(filter $(wildcard %s/*),$(%s)) " pdir var)
-		  inc_ml;
-	printf "\n";
-      end;
-    (* Files in the scope of a -R option (assuming they are disjoint) *)
-    List.iteri (fun i (pdir,_,abspdir) ->
-		if List.exists (is_prefix abspdir) absdir_of_files then
-		  printf "%s%d=$(patsubst %s/%%,%%,$(filter %s/%%,$(%s)))\n"
-			 var i pdir pdir var)
-	       (inc_i@inc_r)
-
-let vars_to_put_by_root var_x_files_l (inc_ml,inc_i,inc_r) =
-  let var_x_absdirs_l =
-    List.rev_map
-      (fun (v,l) ->
-       (v,List.rev_map
-            (fun x -> CUnix.canonical_path_name (Filename.dirname x)) l))
-      var_x_files_l
+    if le >= 0 && Bytes.get ldir le = '.' then Bytes.sub ldir 0 (le - 1)
+    else Bytes.copy ldir
   in
-  let var_filter f g =
-    List.fold_left
-      (fun acc (var,dirs) -> if f dirs then (g var)::acc else acc)
-      [] var_x_absdirs_l
-  in
-  (* All files caught by a -R . option (assuming it is the only one) *)
-  match inc_i@inc_r with
-  |[(".",t,_)] ->
-    (None,[".",physical_dir_of_logical_dir t,List.rev_map fst var_x_files_l])
-  |l ->
-    try
-      let out = List.assoc "." (List.rev_map (fun (p,l,_) -> (p,l)) l) in
-      let () = prerr_string "Warning: install rule assumes that -R/-Q . _ is the only -R/-Q option\n"
-      in
-      (None,[".",physical_dir_of_logical_dir out,List.rev_map fst var_x_files_l])
-    with Not_found ->
-      (* vars for -Q options *)
-      let varq = var_filter
-                   (fun l -> List.exists (fun (_,a) -> List.mem a l) inc_ml)
-                   (fun x -> x)
-      in
-      (* (physical dir, physical dir of logical path,vars) for -R options
-	 (assuming physical dirs are disjoint) *)
-      let other =
-        if l = [] then
-	  [".","$(INSTALLDEFAULTROOT)",[]]
-        else
-	  Util.List.fold_left_i (fun i out (pdir,ldir,abspdir) ->
-	    let vars_r = var_filter
-                           (List.exists (is_prefix abspdir))
-                           (fun x -> x^string_of_int i)
-            in
-	    let pdir' = physical_dir_of_logical_dir ldir in
-	    (pdir,pdir',vars_r)::out) 0 [] l
-      in (Some varq, other)
-
-let install_include_by_root perms =
-  let install_dir for_i (pdir,pdir',vars) =
-    let b = vars <> [] in
-    if b then begin
-      printf "\tcd \"%s\" && for i in " pdir;
-      print_list " " (List.rev_map (Format.sprintf "$(%s)") vars);
-      print "; do \\\n";
-      printf "\t install -d \"`dirname \"$(DSTROOT)\"$(COQLIBINSTALL)/%s/$$i`\"; \\\n" pdir';
-      printf "\t install -m %s $$i \"$(DSTROOT)\"$(COQLIBINSTALL)/%s/$$i; \\\n" perms pdir';
-      printf "\tdone\n";
-    end;
-    for_i b pdir' in
-  let install_i = function
-    |[] -> fun _ _ -> ()
-    |l -> fun b d ->
-      if not b then printf "\tinstall -d \"$(DSTROOT)\"$(COQLIBINSTALL)/%s; \\\n" d;
-      print "\tfor i in ";
-      print_list " " (List.rev_map (Format.sprintf "$(%sINC)") l);
-      print "; do \\\n";
-      printf "\t install -m %s $$i \"$(DSTROOT)\"$(COQLIBINSTALL)/%s/`basename $$i`; \\\n" perms d;
-      printf "\tdone\n"
-  in function
-  |None,l -> List.iter (install_dir (fun _ _ -> ())) l
-  |Some v_i,l -> List.iter (install_dir (install_i v_i)) l
-
-let uninstall_by_root =
-  let uninstall_dir for_i (pdir,pdir',vars) =
-    printf "\tprintf 'cd \"$${DSTROOT}\"$(COQLIBINSTALL)/%s" pdir';
-    if vars <> [] then begin
-      print " && rm -f ";
-      print_list " " (List.rev_map (Format.sprintf "$(%s)") vars);
-    end;
-    for_i ();
-    print " && find . -type d -and -empty -delete\\n";
-    print "cd \"$${DSTROOT}\"$(COQLIBINSTALL) && ";
-    printf "find \"%s\" -maxdepth 0 -and -empty -exec rmdir -p \\{\\} \\;\\n' >> \"$@\"\n" pdir'
-in
-  let uninstall_i = function
-    |[] -> ()
-    |l ->
-      print " && \\\\\\nfor i in ";
-      print_list " " (List.rev_map (Format.sprintf "$(%sINC)") l);
-      print "; do rm -f \"`basename \"$$i\"`\"; done"
-  in function
-  |None,l -> List.iter (uninstall_dir (fun _ -> ())) l
-  |Some v_i,l -> List.iter (uninstall_dir (fun () -> uninstall_i v_i)) l
-
-let where_put_doc = function
-    |_,[],[] -> "$(INSTALLDEFAULTROOT)";
-    |_,((_,lp,_)::q as inc_i),[] ->
-      let pr = List.fold_left (fun a (_,b,_) -> string_prefix a b) lp q in
-      if (pr <> "") &&
-	((List.exists (fun(_,b,_) -> b = pr) inc_i)
-	 || pr.[String.length pr - 1] = '.')
-      then
-	physical_dir_of_logical_dir pr
-      else
-	let () = prerr_string ("Warning: -Q options don't have a correct common prefix,"
-                        ^ " install-doc will put anything in $INSTALLDEFAULTROOT\n") in
-	"$(INSTALLDEFAULTROOT)"
-    |_,inc_i,((_,lp,_)::q as inc_r) ->
-      let pr = List.fold_left (fun a (_,b,_) -> string_prefix a b) lp q in
-      let pr = List.fold_left (fun a (_,b,_) -> string_prefix a b) pr inc_i in
-      if (pr <> "") &&
-	((List.exists (fun(_,b,_) -> b = pr) inc_r)
-	 || (List.exists (fun(_,b,_) -> b = pr) inc_i)
-	 || pr.[String.length pr - 1] = '.')
-      then
-	physical_dir_of_logical_dir pr
-      else
-	let () = prerr_string ("Warning: -R/-Q options don't have a correct common prefix,"
-                        ^ " install-doc will put anything in $INSTALLDEFAULTROOT\n") in
-	"$(INSTALLDEFAULTROOT)"
-
-let install (vfiles,(mlis,ml4s,mls,mllibs,mlpacks),_,sds) inc = function
-  |Project_file.NoInstall -> ()
-  |is_install ->
-    let not_empty = function |[] -> false |_::_ -> true in
-    let cmos = List.rev_append mlpacks (List.rev_append mls ml4s) in
-    let cmis = List.rev_append mlis cmos in
-    let cmxss = List.rev_append cmos mllibs in
-    let where_what_cmxs = vars_to_put_by_root [("CMXSFILES",cmxss)] inc in
-    let where_what_oth = vars_to_put_by_root
-      [("VOFILES",vfiles);("VFILES",vfiles);
-       ("GLOBFILES",vfiles);("NATIVEFILES",vfiles);
-       ("CMOFILES",cmos);("CMIFILES",cmis);("CMAFILES",mllibs)]
-      inc in
-    let doc_dir = where_put_doc inc in
-    if is_install = Project_file.UnspecInstall then begin
-	print "userinstall:\n\t+$(MAKE) USERINSTALL=true install\n\n"
-    end;
-    if not_empty cmxss then begin
-      print "install-natdynlink:\n";
-      install_include_by_root "0755" where_what_cmxs;
-      print "\n";
+  for i = 0 to le - 1 do
+    if Bytes.get pdir i = '.' then Bytes.set pdir i '/';
+  done;
+  Bytes.to_string pdir
+
+let read_whole_file s =
+  let ic = open_in s in
+  let b = Buffer.create (1 lsl 12) in
+  try
+     while true do
+       let s = input_line ic in
+       Buffer.add_string b s;
+       Buffer.add_char b '\n';
+     done;
+     assert false;
+  with End_of_file ->
+    close_in ic;
+    Buffer.contents b
+
+let makefile_template =
+  let open Filename in
+  let template = "/tools/CoqMakefile.in" in
+  if Coq_config.local then
+    let coqbin = CUnix.canonical_path_name (dirname Sys.executable_name) in
+    dirname coqbin ^ template
+  else match Coq_config.coqlib with
+    | None -> assert false
+    | Some dir -> dir ^ template
+
+let quote s = if String.contains s ' ' then "\"" ^ s ^ "\"" else s
+
+let generate_makefile oc conf_file local_file args project =
+  let s = read_whole_file makefile_template in
+  let s = List.fold_left
+    (fun s (k,v) -> Str.global_replace (Str.regexp_string k) v s) s
+    [ "@CONF_FILE@", conf_file;
+      "@LOCAL_FILE@", local_file;
+      "@COQ_VERSION@", Coq_config.version;
+      "@PROJECT_FILE@", (Option.default "" project.project_file);
+      "@COQ_MAKEFILE_INVOCATION@",String.concat " " (List.map quote args);
+    ] in
+  output_string oc s
+;;
+
+let section oc s =
+  let pad = String.make (76 - String.length s) ' ' in
+  let sharps = String.make 79 '#' in
+  let spaces = "#" ^ String.make 77 ' ' ^ "#" in
+  fprintf oc "\n%s\n" sharps;
+  fprintf oc "%s\n" spaces;
+  fprintf oc "# %s%s#\n" s pad;
+  fprintf oc "%s\n" spaces;
+  fprintf oc "%s\n\n" sharps
+;;
+
+let clean_tgts = ["clean"; "cleanall"; "archclean"]
+
+let generate_conf_extra_target oc sps =
+  let pr_path { target; dependencies; phony; command } =
+    let target = if target = "all" then "custom-all" else target in
+    if phony then fprintf oc ".PHONY: %s\n" target;
+    if not (is_genrule target) && not phony then begin
+      fprintf oc "post-all::\n\t$(MAKE) -f $(SELF) %s\n" target;
+      if not phony then
+        fprintf oc "clean::\n\trm -f %s\n" target;
     end;
-    if not_empty cmxss then begin
-      print "install-toploop: $(MLLIBFILES:.mllib=.cmxs)\n";
-      printf "\t install -d \"$(DSTROOT)\"$(COQTOPINSTALL)/\n";
-      printf "\t install -m 0755 $?  \"$(DSTROOT)\"$(COQTOPINSTALL)/\n";
-      print "\n";
-    end;
-    print "install:";
-    if not_empty cmxss then begin
-      print "$(if $(HASNATDYNLINK_OR_EMPTY),install-natdynlink)";
-    end;
-    print "\n";
-    install_include_by_root "0644" where_what_oth;
-    List.iter
-      (fun x ->
-	printf "\t+cd %s && $(MAKE) DSTROOT=\"$(DSTROOT)\" INSTALLDEFAULTROOT=\"$(INSTALLDEFAULTROOT)/%s\" install\n" x x)
-      sds;
-    print "\n";
-    let install_one_kind kind dir =
-      printf "\tinstall -d \"$(DSTROOT)\"$(COQDOCINSTALL)/%s/%s\n" dir kind;
-      printf "\tfor i in %s/*; do \\\n" kind;
-      printf "\t install -m 0644 $$i \"$(DSTROOT)\"$(COQDOCINSTALL)/%s/$$i;\\\n" dir;
-      print "\tdone\n" in
-    print "install-doc:\n";
-    if not_empty vfiles then install_one_kind "html" doc_dir;
-    if not_empty mlis then install_one_kind "mlihtml" doc_dir;
-    print "\n";
-    let uninstall_one_kind kind dir =
-      printf "\tprintf 'cd \"$${DSTROOT}\"$(COQDOCINSTALL)/%s \\\\\\n' >> \"$@\"\n" dir;
-      printf "\tprintf '&& rm -f $(shell find \"%s\" -maxdepth 1 -and -type f -print)\\n' >> \"$@\"\n" kind;
-      print "\tprintf 'cd \"$${DSTROOT}\"$(COQDOCINSTALL) && ";
-      printf "find %s/%s -maxdepth 0 -and -empty -exec rmdir -p \\{\\} \\;\\n' >> \"$@\"\n" dir kind
-    in
-    printf "uninstall_me.sh: %s\n" !makefile_name;
-    print "\techo '#!/bin/sh' > $@\n";
-    if not_empty cmxss then uninstall_by_root where_what_cmxs;
-    uninstall_by_root where_what_oth;
-    if not_empty vfiles then uninstall_one_kind "html" doc_dir;
-    if not_empty mlis then uninstall_one_kind "mlihtml" doc_dir;
-    print "\tchmod +x $@\n";
-    print "\n";
-    print "uninstall: uninstall_me.sh\n";
-    print "\tsh $<\n\n"
-
-let make_makefile sds =
-  if !make_name <> "" then begin
-    printf "%s: %s\n" !makefile_name !make_name;
-    print "\tmv -f $@ $@.bak\n";
-    print "\t\"$(COQBIN)coq_makefile\" -f $< -o $@\n\n";
-    List.iter
-      (fun x -> print "\t+cd "; print x; print " && $(MAKE) Makefile\n")
-      sds;
-    print "\n";
-  end
-
-let clean sds sps =
-  print "clean::\n";
-  if !some_mlfile || !some_mlifile || !some_ml4file
-     || !some_mllibfile || !some_mlpackfile
-  then
-    begin
-      print "\trm -f $(ALLCMOFILES) $(CMIFILES) $(CMAFILES)\n";
-      print "\trm -f $(ALLCMOFILES:.cmo=.cmx) $(CMXAFILES) $(CMXSFILES) $(ALLCMOFILES:.cmo=.o) $(CMXAFILES:.cmxa=.a)\n";
-      print "\trm -f $(addsuffix .d,$(MLFILES) $(MLIFILES) $(ML4FILES) $(MLLIBFILES) $(MLPACKFILES))\n";
-    end;
-  if !some_vfile then
-    begin
-      print "\trm -f $(OBJFILES) $(OBJFILES:.o=.native) $(NATIVEFILES)\n";
-      print "\tfind . -name .coq-native -type d -empty -delete\n";
-      print "\trm -f $(VOFILES) $(VOFILES:.vo=.vio) $(GFILES) $(VFILES:.v=.v.d) $(VFILES:=.beautified) $(VFILES:=.old)\n"
-    end;
-  print "\trm -f all.ps all-gal.ps all.pdf all-gal.pdf all.glob $(VFILES:.v=.glob) $(VFILES:.v=.tex) $(VFILES:.v=.g.tex) all-mli.tex\n";
-  print "\t- rm -rf html mlihtml uninstall_me.sh\n";
-  List.iter
-    (fun (file,_,is_phony,_) ->
-       if not (is_phony || is_genrule file) then
-	 (print "\t- rm -rf "; print file; print "\n"))
-    sps;
-  List.iter
-    (fun x -> print "\t+cd "; print x; print " && $(MAKE) clean\n")
-    sds;
-  print "\n";
-  let () =
-    if !some_vfile then
-      let () = print "cleanall:: clean\n" in
-      print "\trm -f $(foreach f,$(VFILES:.v=),$(dir $(f)).$(notdir $(f)).aux)\n\n" in
-  print "archclean::\n";
-  print "\trm -f *.cmx *.o\n";
-  List.iter
-    (fun x -> print "\t+cd "; print x; print " && $(MAKE) archclean\n")
-    sds;
-  print "\n";
-  print "printenv:\n\t@\"$(COQBIN)coqtop\" -config\n";
-  print "\t@echo 'OCAMLFIND =\t$(OCAMLFIND)'\n\t@echo 'PP =\t$(PP)'\n\t@echo 'COQFLAGS =\t$(COQFLAGS)'\n";
-  print "\t@echo 'COQLIBINSTALL =\t$(COQLIBINSTALL)'\n\t@echo 'COQDOCINSTALL =\t$(COQDOCINSTALL)'\n\n"
-
-let header_includes () = ()
-
-let implicit () =
-    section "Implicit rules.";
-  let mli_rules () =
-    print "$(MLIFILES:.mli=.cmi): %.cmi: %.mli\n";
-    print "\t$(SHOW)'CAMLC -c $<'\n";
-    print "\t$(HIDE)$(CAMLC) $(ZDEBUG) $(ZFLAGS) $<\n\n";
-    print "$(addsuffix .d,$(MLIFILES)): %.mli.d: %.mli\n";
-    print "\t$(SHOW)'CAMLDEP $<'\n";
-    print "\t$(HIDE)$(CAMLDEP) $(OCAMLLIBS) \"$<\" > \"$@\" || ( RV=$$?; rm -f \"$@\"; exit $${RV} )\n\n"
-  in
-  let ml4_rules () =
-    print "$(ML4FILES:.ml4=.cmo): %.cmo: %.ml4\n";
-    print "\t$(SHOW)'CAMLC -pp -c $<'\n";
-    print "\t$(HIDE)$(CAMLC) $(ZDEBUG) $(ZFLAGS) $(PP) -impl $<\n\n";
-    print "$(filter-out $(addsuffix .cmx,$(foreach lib,$(MLPACKFILES:.mlpack=_MLPACK_DEPENDENCIES),$($(lib)))),$(ML4FILES:.ml4=.cmx)): %.cmx: %.ml4\n";
-    print "\t$(SHOW)'CAMLOPT -pp -c $<'\n";
-    print "\t$(HIDE)$(CAMLOPTC) $(ZDEBUG) $(ZFLAGS) $(PP) -impl $<\n\n";
-    print "$(addsuffix .d,$(ML4FILES)): %.ml4.d: %.ml4\n";
-    print "\t$(SHOW)'CAMLDEP -pp $<'\n";
-    print "\t$(HIDE)$(CAMLDEP) $(OCAMLLIBS) $(PP) -impl \"$<\" > \"$@\" || ( RV=$$?; rm -f \"$@\"; exit $${RV} )\n\n" in
-  let ml_rules () =
-    print "$(MLFILES:.ml=.cmo): %.cmo: %.ml\n";
-    print "\t$(SHOW)'CAMLC -c $<'\n";
-    print "\t$(HIDE)$(CAMLC) $(ZDEBUG) $(ZFLAGS) $<\n\n";
-    print "$(filter-out $(addsuffix .cmx,$(foreach lib,$(MLPACKFILES:.mlpack=_MLPACK_DEPENDENCIES),$($(lib)))),$(MLFILES:.ml=.cmx)): %.cmx: %.ml\n";
-    print "\t$(SHOW)'CAMLOPT -c $<'\n";
-    print "\t$(HIDE)$(CAMLOPTC) $(ZDEBUG) $(ZFLAGS) $<\n\n";
-    print "$(addsuffix .d,$(MLFILES)): %.ml.d: %.ml\n";
-    print "\t$(SHOW)'CAMLDEP $<'\n";
-    print "\t$(HIDE)$(CAMLDEP) $(OCAMLLIBS) \"$<\" > \"$@\" || ( RV=$$?; rm -f \"$@\"; exit $${RV} )\n\n" in
-  let cmxs_rules () = (* order is important here when there is foo.ml and foo.mllib *)
-    print "$(filter-out $(MLLIBFILES:.mllib=.cmxs),$(MLFILES:.ml=.cmxs) $(ML4FILES:.ml4=.cmxs) $(MLPACKFILES:.mlpack=.cmxs)): %.cmxs: %.cmx\n";
-    print "\t$(SHOW)'CAMLOPT -shared -o $@'\n";
-    print "\t$(HIDE)$(CAMLOPTLINK) $(ZDEBUG) $(ZFLAGS) -shared -o $@ $<\n\n";
-    print "$(MLLIBFILES:.mllib=.cmxs): %.cmxs: %.cmxa\n";
-    print "\t$(SHOW)'CAMLOPT -shared -o $@'\n";
-    print "\t$(HIDE)$(CAMLOPTLINK) $(ZDEBUG) $(ZFLAGS) -linkall -shared -o $@ $<\n\n"
-  in
-  let mllib_rules () =
-    print "$(MLLIBFILES:.mllib=.cma): %.cma: | %.mllib\n";
-    print "\t$(SHOW)'CAMLC -a -o $@'\n";
-    print "\t$(HIDE)$(CAMLLINK) $(ZDEBUG) $(ZFLAGS) -a -o $@ $^\n\n";
-    print "$(MLLIBFILES:.mllib=.cmxa): %.cmxa: | %.mllib\n";
-    print "\t$(SHOW)'CAMLOPT -a -o $@'\n";
-    print "\t$(HIDE)$(CAMLOPTLINK) $(ZDEBUG) $(ZFLAGS) -a -o $@ $^\n\n";
-    print "$(addsuffix .d,$(MLLIBFILES)): %.mllib.d: %.mllib\n";
-    print "\t$(SHOW)'COQDEP $<'\n";
-    print "\t$(HIDE)$(COQDEP) $(OCAMLLIBS) -c \"$<\" > \"$@\" || ( RV=$$?; rm -f \"$@\"; exit $${RV} )\n\n"
-  in
-  let mlpack_rules () =
-    print "$(MLPACKFILES:.mlpack=.cmo): %.cmo: | %.mlpack\n";
-    print "\t$(SHOW)'CAMLC -pack -o $@'\n";
-    print "\t$(HIDE)$(CAMLLINK) $(ZDEBUG) $(ZFLAGS) -pack -o $@ $^\n\n";
-    print "$(MLPACKFILES:.mlpack=.cmx): %.cmx: | %.mlpack\n";
-    print "\t$(SHOW)'CAMLOPT -pack -o $@'\n";
-    print "\t$(HIDE)$(CAMLOPTLINK) $(ZDEBUG) $(ZFLAGS) -pack -o $@ $^\n\n";
-    print "$(addsuffix .d,$(MLPACKFILES)): %.mlpack.d: %.mlpack\n";
-    print "\t$(SHOW)'COQDEP $<'\n";
-    print "\t$(HIDE)$(COQDEP) $(OCAMLLIBS) -c \"$<\" > \"$@\" || ( RV=$$?; rm -f \"$@\"; exit $${RV} )\n\n"
-  in
-  let v_rules () =
-    print "$(VOFILES): %.vo: %.v\n";
-    print "\t$(SHOW)COQC $<\n";
-    print "\t$(HIDE)$(COQC) $(COQDEBUG) $(COQFLAGS) $<\n\n";
-    print "$(GLOBFILES): %.glob: %.v\n\t$(COQC) $(COQDEBUG) $(COQFLAGS) $<\n\n";
-    print "$(VFILES:.v=.vio): %.vio: %.v\n\t$(COQC) -quick $(COQDEBUG) $(COQFLAGS) $<\n\n";
-    print "$(GFILES): %.g: %.v\n\t$(GALLINA) $<\n\n";
-    print "$(VFILES:.v=.tex): %.tex: %.v\n\t$(COQDOC) $(COQDOCFLAGS) -latex $< -o $@\n\n";
-    print "$(HTMLFILES): %.html: %.v %.glob\n\t$(COQDOC) $(COQDOCFLAGS) -html $< -o $@\n\n";
-    print "$(VFILES:.v=.g.tex): %.g.tex: %.v\n\t$(COQDOC) $(COQDOCFLAGS) -latex -g $< -o $@\n\n";
-    print "$(GHTMLFILES): %.g.html: %.v %.glob\n\t$(COQDOC) $(COQDOCFLAGS)  -html -g $< -o $@\n\n";
-    print "$(addsuffix .d,$(VFILES)): %.v.d: %.v\n";
-    print "\t$(SHOW)'COQDEP $<'\n";
-    print "\t$(HIDE)$(COQDEP) $(COQLIBS) \"$<\" > \"$@\" || ( RV=$$?; rm -f \"$@\"; exit $${RV} )\n\n";
-    print "$(addsuffix .beautified,$(VFILES)): %.v.beautified:\n\t$(COQC) $(COQDEBUG) $(COQFLAGS) -beautify $*.v\n\n"
-  in
-    if !some_mlifile then mli_rules ();
-    if !some_ml4file then ml4_rules ();
-    if !some_mlfile then ml_rules ();
-    if !some_mlfile || !some_ml4file then cmxs_rules ();
-    if !some_mllibfile then mllib_rules ();
-    if !some_mlpackfile then mlpack_rules ();
-    if !some_vfile then v_rules ()
-
-let variables is_install opt (args,defs) =
-  let var_aux (v,def) = print v; print "="; print def; print "\n" in
-    section "Variables definitions.";
-    List.iter var_aux defs;
-    print "\n";
-    if not opt then
-      print "override OPT:=-byte\n"
-    else
-      print "OPT?=\n";
-    begin
-      match args with
-	|[] -> ()
-	|h::t -> print "OTHERFLAGS=";
-	  print h;
-	  List.iter (fun s -> print " ";print s) t;
-	  print "\n";
-    end;
-    (* Coq executables and relative variables *)
-    if !some_vfile || !some_mlpackfile || !some_mllibfile then
-      print "COQDEP?=\"$(COQBIN)coqdep\" -c\n";
-    if !some_vfile then begin
-    print "COQFLAGS?=-q $(OPT) $(COQLIBS) $(OTHERFLAGS) $(COQ_XML)\n";
-    print "COQCHKFLAGS?=-silent -o\n";
-    print "COQDOCFLAGS?=-interpolate -utf8\n";
-    print "COQC?=$(TIMER) \"$(COQBIN)coqc\"\n";
-    print "GALLINA?=\"$(COQBIN)gallina\"\n";
-    print "COQDOC?=\"$(COQBIN)coqdoc\"\n";
-    print "COQCHK?=\"$(COQBIN)coqchk\"\n";
-    print "COQMKTOP?=\"$(COQBIN)coqmktop\"\n\n";
-    end;
-    (* Caml executables and relative variables *)
-    if !some_ml4file || !some_mlfile || !some_mlifile then begin
-    print "COQSRCLIBS?=" ;
-    List.iter (fun c -> print "-I \"$(COQLIB)"; print c ; print "\" \\\n") lib_dirs ;
-    List.iter (fun c -> print " \\\
-\n  -I \"$(COQLIB)/"; print c; print "\"") Coq_config.plugins_dirs; print "\n";
-    print "ZFLAGS=$(OCAMLLIBS) $(COQSRCLIBS) -I $(CAMLP4LIB)\n\n";
-    print "CAMLC?=$(OCAMLFIND) ocamlc -c -rectypes -thread -safe-string\n";
-    print "CAMLOPTC?=$(OCAMLFIND) opt -c -rectypes -thread -safe-string\n";
-    print "CAMLLINK?=$(OCAMLFIND) ocamlc -rectypes -thread -safe-string\n";
-    print "CAMLOPTLINK?=$(OCAMLFIND) opt -rectypes -thread -safe-string\n";
-    print "CAMLDEP?=$(OCAMLFIND) ocamldep -slash -ml-synonym .ml4 -ml-synonym .mlpack\n";
-    print "CAMLLIB?=$(shell $(OCAMLFIND) printconf stdlib)\n";
-    print "GRAMMARS?=grammar.cma\n";
-    print "CAMLP4EXTEND=pa_extend.cmo q_MLast.cmo pa_macro.cmo\n";
-    print "PP?=-pp '$(CAMLP4O) -I $(CAMLLIB) -I $(COQLIB)/grammar compat5.cmo \\\
-\n  $(CAMLP4EXTEND) $(GRAMMARS) $(CAMLP4OPTIONS) -impl'\n\n";
-    end;
-    match is_install with
-      | Project_file.NoInstall -> ()
-      | Project_file.UnspecInstall ->
-        section "Install Paths.";
-	print "ifdef USERINSTALL\n";
-        print "XDG_DATA_HOME?=\"$(HOME)/.local/share\"\n";
-        print "COQLIBINSTALL=$(XDG_DATA_HOME)/coq\n";
-        print "COQDOCINSTALL=$(XDG_DATA_HOME)/doc/coq\n";
-	print "else\n";
-        print "COQLIBINSTALL=\"${COQLIB}user-contrib\"\n";
-        print "COQDOCINSTALL=\"${DOCDIR}user-contrib\"\n";
-        print "COQTOPINSTALL=\"${COQLIB}toploop\"\n";
-	print "endif\n\n"
-      | Project_file.TraditionalInstall ->
-          section "Install Paths.";
-          print "COQLIBINSTALL=\"${COQLIB}user-contrib\"\n";
-          print "COQDOCINSTALL=\"${DOCDIR}user-contrib\"\n";
-          print "COQTOPINSTALL=\"${COQLIB}toploop\"\n";
-          print "\n"
-      | Project_file.UserInstall ->
-          section "Install Paths.";
-          print "XDG_DATA_HOME?=\"$(HOME)/.local/share\"\n";
-          print "COQLIBINSTALL=$(XDG_DATA_HOME)/coq\n";
-          print "COQDOCINSTALL=$(XDG_DATA_HOME)/doc/coq\n";
-          print "COQTOPINSTALL=$(XDG_DATA_HOME)/coq/toploop\n";
-          print "\n"
-
-let parameters () =
-  print ".DEFAULT_GOAL := all\n\n";
-  print "# This Makefile may take arguments passed as environment variables:\n";
-  print "# COQBIN to specify the directory where Coq binaries resides;\n";
-  print "# TIMECMD set a command to log .v compilation time;\n";
-  print "# TIMED if non empty, use the default time command as TIMECMD;\n";
-  print "# ZDEBUG/COQDEBUG to specify debug flags for ocamlc&ocamlopt/coqc;\n";
-  print "# DSTROOT to specify a prefix to install path.\n";
-  print "# VERBOSE to disable the short display of compilation rules.\n\n";
-  print "VERBOSE?=\n";
-  print "SHOW := $(if $(VERBOSE),@true \"\",@echo \"\")\n";
-  print "HIDE := $(if $(VERBOSE),,@)\n\n";
-  print "# Here is a hack to make $(eval $(shell works:\n";
-  print "define donewline\n\n\nendef\n";
-  print "includecmdwithout@ = $(eval $(subst @,$(donewline),$(shell { $(1) | tr -d '\\r' | tr '\\n' '@'; })))\n";
-  print "$(call includecmdwithout@,$(COQBIN)coqtop -config)\n\n";
-  print "TIMED?=\nTIMECMD?=\nSTDTIME?=/usr/bin/time -f \"$* (user: %U mem: %M ko)\"\n";
-  print "TIMER=$(if $(TIMED), $(STDTIME), $(TIMECMD))\n\n";
-  print "vo_to_obj = $(addsuffix .o,\\\n";
-  print "  $(filter-out Warning: Error:,\\\n";
-  print "  $(shell $(COQBIN)coqtop -q -noinit -batch -quiet -print-mod-uid $(1))))\n\n"
-
-let include_dirs (inc_ml,inc_q,inc_r) =
-  let parse_ml_includes l = List.map (fun (x,_) -> "-I \"" ^ x ^ "\"") l in
-  let includes =
-    List.map (fun (p,l,_) ->
-              let l' = if l = "" then "\"\"" else l in
-              " \"" ^ p ^ "\" " ^ l' ^"") in
-  let str_ml = parse_ml_includes inc_ml in
-  section "Libraries definitions.";
-  if !some_ml4file || !some_mlfile || !some_mlifile then begin
-    print "OCAMLLIBS?="; print_list "\\\n  " str_ml; print "\n";
-  end;
-  if !some_vfile || !some_mllibfile || !some_mlpackfile then begin
-    print "COQLIBS?=";
-    print_prefix_list "\\\n  -Q" (includes inc_q);
-    print_prefix_list "\\\n  -R" (includes inc_r);
-    print_prefix_list "\\\n  " str_ml;
-    print "\n";
-  end;
-  if !some_vfile then begin
-    print "COQCHKLIBS?=";
-    print_prefix_list "\\\n  -R" (includes inc_q);
-    print_prefix_list "\\\n  -R" (includes inc_r);
-    print "\n";
-    print "COQDOCLIBS?=";
-    print_prefix_list "\\\n  -R" (includes inc_q);
-    print_prefix_list "\\\n  -R" (includes inc_r);
-    print "\n";
-  end;
-  print "\n"
-
-let double_colon = ["clean"; "cleanall"; "archclean"]
-
-let custom sps =
-  let pr_path (file,dependencies,is_phony,com) =
-    print file;
-    print (if List.mem file double_colon then ":: " else ": ");
-    print dependencies; print "\n";
-    if com <> "" then (print "\t"; print com; print "\n");
-    print "\n"
+    fprintf oc "%s %s %s\n\t%s\n\n"
+       target
+       (if List.mem target clean_tgts then ":: " else ": ")
+       dependencies
+       command
   in
-    if sps <> [] then section "Custom targets.";
+    if sps <> [] then
+      section oc "Extra targets. (-extra and -extra-phony, DEPRECATED)";
     List.iter pr_path sps
 
-let subdirs sds =
-  let pr_subdir s =
-    print s; print ":\n\t+cd \""; print s; print "\" && $(MAKE) all\n\n"
-  in
-  if sds <> [] then
-    let () =
-      Format.eprintf "@[Warning: Targets for subdirectories are very fragile.@ " in
-    let () =
-      Format.eprintf "For example,@ nothing is done to handle dependencies@ with them.@]@." in
-      section "Subdirectories.";
-    List.iter pr_subdir sds
-
-let forpacks l =
-  let () = if l <> [] then section "Ad-hoc implicit rules for mlpack." in
-  List.iter (fun it ->
-    let h = Filename.chop_extension it in
-    let pk = String.capitalize (Filename.basename h) in
-    printf "$(addsuffix .cmx,$(filter $(basename $(MLFILES)),$(%s_MLPACK_DEPENDENCIES))): %%.cmx: %%.ml\n" h;
-    printf "\t$(SHOW)'CAMLOPT -c -for-pack %s $<'\n" pk;
-    printf "\t$(HIDE)$(CAMLOPTC) $(ZDEBUG) $(ZFLAGS) -for-pack %s $<\n\n" pk;
-    printf "$(addsuffix .cmx,$(filter $(basename $(ML4FILES)),$(%s_MLPACK_DEPENDENCIES))): %%.cmx: %%.ml4\n" h;
-    printf "\t$(SHOW)'CAMLOPT -c -pp -for-pack %s $<'\n" pk;
-    printf "\t$(HIDE)$(CAMLOPTC) $(ZDEBUG) $(ZFLAGS) -for-pack %s $(PP) -impl $<\n\n" pk
-  ) l
-
-let main_targets vfiles (mlifiles,ml4files,mlfiles,mllibfiles,mlpackfiles) other_targets inc =
-  let decl_var var = function
-    |[] -> ()
-    |l ->
-      printf "%s:=" var; print_list "\\\n  " l; print "\n\n";
-      print "ifneq ($(filter-out archclean clean cleanall printenv,$(MAKECMDGOALS)),)\n";
-      printf "-include $(addsuffix .d,$(%s))\n" var;
-      print "else\nifeq ($(MAKECMDGOALS),)\n";
-      printf "-include $(addsuffix .d,$(%s))\n" var;
-      print "endif\nendif\n\n";
-      printf ".SECONDARY: $(addsuffix .d,$(%s))\n\n" var
-  in
-  section "Files dispatching.";
-  decl_var "VFILES" vfiles;
-  begin match vfiles with
-    |[] -> ()
-    |l ->
-      print "VO=vo\n";
-      print "VOFILES:=$(VFILES:.v=.$(VO))\n";
-      classify_files_by_root "VOFILES" l inc;
-      classify_files_by_root "VFILES" l inc;
-      print "GLOBFILES:=$(VFILES:.v=.glob)\n";
-      print "GFILES:=$(VFILES:.v=.g)\n";
-      print "HTMLFILES:=$(VFILES:.v=.html)\n";
-      print "GHTMLFILES:=$(VFILES:.v=.g.html)\n";
-      print "OBJFILES=$(call vo_to_obj,$(VOFILES))\n";
-      print "ALLNATIVEFILES=$(OBJFILES:.o=.cmi) $(OBJFILES:.o=.cmo) $(OBJFILES:.o=.cmx) $(OBJFILES:.o=.cmxs)\n";
-      print "NATIVEFILES=$(foreach f, $(ALLNATIVEFILES), $(wildcard $f))\n";
-      classify_files_by_root "NATIVEFILES" l inc
-  end;
-  decl_var "ML4FILES" ml4files;
-  decl_var "MLFILES" mlfiles;
-  decl_var "MLPACKFILES" mlpackfiles;
-  decl_var "MLLIBFILES" mllibfiles;
-  decl_var "MLIFILES" mlifiles;
-  let mlsfiles = match ml4files,mlfiles,mlpackfiles with
-    |[],[],[] -> []
-    |[],[],_ -> Printf.eprintf "Mlpack cannot work without ml[4]?"; []
-    |[],ml,[] ->
-      print "ALLCMOFILES:=$(MLFILES:.ml=.cmo)\n";
-      ml
-    |ml4,[],[] ->
-      print "ALLCMOFILES:=$(ML4FILES:.ml4=.cmo)\n";
-      ml4
-    |ml4,ml,[] ->
-      print "ALLCMOFILES:=$(ML4FILES:.ml4=.cmo) $(MLFILES:.ml=.cmo)\n";
-      List.rev_append ml ml4
-    |[],ml,mlpack ->
-      print "ALLCMOFILES:=$(MLFILES:.ml=.cmo) $(MLPACKFILES:.mlpack=.cmo)\n";
-      List.rev_append mlpack ml
-    |ml4,[],mlpack ->
-      print "ALLCMOFILES:=$(ML4FILES:.ml4=.cmo) $(MLPACKFILES:.mlpack=.cmo)\n";
-      List.rev_append mlpack ml4
-    |ml4,ml,mlpack ->
-      print "ALLCMOFILES:=$(ML4FILES:.ml4=.cmo) $(MLFILES:.ml=.cmo) $(MLPACKFILES:.mlpack=.cmo)\n";
-      List.rev_append mlpack (List.rev_append ml ml4) in
-  begin match mlsfiles with
-    |[] -> ()
-    |l ->
-  print "CMOFILES=$(filter-out $(addsuffix .cmo,$(foreach lib,$(MLLIBFILES:.mllib=_MLLIB_DEPENDENCIES) $(MLPACKFILES:.mlpack=_MLPACK_DEPENDENCIES),$($(lib)))),$(ALLCMOFILES))\n";
-      classify_files_by_root "CMOFILES" l inc;
-      print "CMXFILES=$(CMOFILES:.cmo=.cmx)\n";
-      print "OFILES=$(CMXFILES:.cmx=.o)\n";
-  end;
-  begin match mllibfiles with
-    |[] -> ()
-    |l ->
-      print "CMAFILES:=$(MLLIBFILES:.mllib=.cma)\n";
-	classify_files_by_root "CMAFILES" l inc;
-      print "CMXAFILES:=$(CMAFILES:.cma=.cmxa)\n";
-  end;
-  begin match mlifiles,mlsfiles with
-    |[],[] -> ()
-    |l,[] ->
-       print "CMIFILES:=$(MLIFILES:.mli=.cmi)\n";
-	classify_files_by_root "CMIFILES" l inc;
-    |[],l ->
-      print "CMIFILES=$(ALLCMOFILES:.cmo=.cmi)\n";
-      classify_files_by_root "CMIFILES" l inc;
-    |l1,l2 ->
-      print "CMIFILES=$(sort $(ALLCMOFILES:.cmo=.cmi) $(MLIFILES:.mli=.cmi))\n";
-      classify_files_by_root "CMIFILES" (l1@l2) inc;
-  end;
-  begin match mllibfiles,mlsfiles with
-    |[],[] -> ()
-    |l,[] ->
-      print "CMXSFILES:=$(CMXAFILES:.cmxa=.cmxs)\n";
-      classify_files_by_root "CMXSFILES" l inc;
-    |[],l ->
-      print "CMXSFILES=$(CMXFILES:.cmx=.cmxs)\n";
-      classify_files_by_root "CMXSFILES" l inc;
-    |l1,l2 ->
-      print "CMXSFILES=$(CMXFILES:.cmx=.cmxs) $(CMXAFILES:.cmxa=.cmxs)\n";
-      classify_files_by_root "CMXSFILES" (l1@l2) inc;
-  end;
-  print "ifeq '$(HASNATDYNLINK)' 'true'\n";
-  print "HASNATDYNLINK_OR_EMPTY := yes\n";
-  print "else\n";
-  print "HASNATDYNLINK_OR_EMPTY :=\n";
-  print "endif\n\n";
-  section "Definition of the toplevel targets.";
-  print "all: ";
-  if !some_vfile then print "$(VOFILES) ";
-  if !some_mlfile || !some_ml4file || !some_mlpackfile then print "$(CMOFILES) ";
-  if !some_mllibfile then print "$(CMAFILES) ";
-  if !some_mlfile || !some_ml4file || !some_mllibfile || !some_mlpackfile
-  then print "$(if $(HASNATDYNLINK_OR_EMPTY),$(CMXSFILES)) ";
-  print_list "\\\n  " other_targets; print "\n\n";
-  if !some_mlifile then
-    begin
-      print "mlihtml: $(MLIFILES:.mli=.cmi)\n";
-      print "\t mkdir $@ || rm -rf $@/*\n";
-      print "\t$(OCAMLFIND) ocamldoc -html -safe-string -rectypes -d $@ -m A $(ZDEBUG) $(ZFLAGS) $(^:.cmi=.mli)\n\n";
-      print "all-mli.tex: $(MLIFILES:.mli=.cmi)\n";
-      print "\t$(OCAMLFIND) ocamldoc -latex -safe-string -rectypes -o $@ -m A $(ZDEBUG) $(ZFLAGS) $(^:.cmi=.mli)\n\n";
-    end;
-  if !some_vfile then
-    begin
-      print "quick: $(VOFILES:.vo=.vio)\n\n";
-      print "vio2vo:\n\t$(COQC) $(COQDEBUG) $(COQFLAGS) -schedule-vio2vo $(J) $(VOFILES:%.vo=%.vio)\n";
-      print "checkproofs:\n\t$(COQC) $(COQDEBUG) $(COQFLAGS) -schedule-vio-checking $(J) $(VOFILES:%.vo=%.vio)\n";
-      print "gallina: $(GFILES)\n\n";
-      print "html: $(GLOBFILES) $(VFILES)\n";
-      print "\t- mkdir -p html\n";
-      print "\t$(COQDOC) -toc $(COQDOCFLAGS) -html $(COQDOCLIBS) -d html $(VFILES)\n\n";
-      print "gallinahtml: $(GLOBFILES) $(VFILES)\n";
-      print "\t- mkdir -p html\n";
-      print "\t$(COQDOC) -toc $(COQDOCFLAGS) -html -g $(COQDOCLIBS) -d html $(VFILES)\n\n";
-      print "all.ps: $(VFILES)\n";
-      print "\t$(COQDOC) -toc $(COQDOCFLAGS) -ps $(COQDOCLIBS) -o $@ `$(COQDEP) -sort -suffix .v $^`\n\n";
-      print "all-gal.ps: $(VFILES)\n";
-      print "\t$(COQDOC) -toc $(COQDOCFLAGS) -ps -g $(COQDOCLIBS) -o $@ `$(COQDEP) -sort -suffix .v $^`\n\n";
-      print "all.pdf: $(VFILES)\n";
-      print "\t$(COQDOC) -toc $(COQDOCFLAGS) -pdf $(COQDOCLIBS) -o $@ `$(COQDEP) -sort -suffix .v $^`\n\n";
-      print "all-gal.pdf: $(VFILES)\n";
-      print "\t$(COQDOC) -toc $(COQDOCFLAGS) -pdf -g $(COQDOCLIBS) -o $@ `$(COQDEP) -sort -suffix .v $^`\n\n";
-      print "validate: $(VOFILES)\n";
-      print "\t$(COQCHK) $(COQCHKFLAGS) $(COQCHKLIBS) $(notdir $(^:.vo=))\n\n";
-      print "beautify: $(VFILES:=.beautified)\n";
-      print "\tfor file in $^; do mv $${file%.beautified} $${file%beautified}old && mv $${file} $${file%.beautified}; done\n";
-      print "\t@echo \'Do not do \"make clean\" until you are sure that everything went well!\'\n";
-      print "\t@echo \'If there were a problem, execute \"for file in $$(find . -name \\*.v.old -print); do mv $${file} $${file%.old}; done\" in your shell/'\n\n"
-    end
-
-let all_target (vfiles, (_,_,_,_,mlpackfiles as mlfiles), sps, sds) inc =
-  let other_targets =
-    CList.map_filter
-      (fun (n,_,is_phony,_) -> if not (is_phony || is_genrule n) then Some n else None)
-      sps @ sds in
-  main_targets vfiles mlfiles other_targets inc;
-  print ".PHONY: ";
-  print_list
-    " "
-    ("all" :: "archclean" :: "beautify" :: "byte" :: "clean" :: "cleanall"
-     :: "gallina" :: "gallinahtml" :: "html" :: "install" :: "install-doc"
-     :: "install-natdynlink" :: "install-toploop" :: "opt" :: "printenv"
-     :: "quick" :: "uninstall" :: "userinstall" :: "validate" :: "vio2vo"
-     :: (sds@(CList.map_filter
-		(fun (n,_,is_phony,_) ->
-		 if is_phony then Some n else None) sps)));
-  print "\n\n";
-  custom sps;
-  subdirs sds;
-  forpacks mlpackfiles
-
-let banner () =
-  print (Printf.sprintf
-"#############################################################################\
-\n##  v      #                   The Coq Proof Assistant                     ##\
-\n## <O___,, #                INRIA - CNRS - LIX - LRI - PPS                 ##\
-\n##   \\VV/  #                                                               ##\
-\n##    //   #  Makefile automagically generated by coq_makefile V%s ##\
-\n#############################################################################\
-\n\n"
-(Coq_config.version ^ String.make (10 - String.length Coq_config.version) ' '))
-
-let warning () =
-  print "# WARNING\n#\n";
-  print "# This Makefile has been automagically generated\n";
-  print "# Edit at your own risks !\n";
-  print "#\n# END OF WARNING\n\n"
-
-let print_list l = List.iter (fun x -> print x; print " ") l
-
-let command_line args =
-  print "#\n# This Makefile was generated by the command line :\n";
-  print "# coq_makefile ";
-  print_list args;
-  print "\n#\n\n"
-
-let ensure_root_dir (vfiles,(mlis,ml4s,mls,mllibs,mlpacks),_,_) inc =
-  let (ml_inc,i_inc,r_inc) = inc in
+let generate_conf_subdirs oc sds =
+  if sds <> [] then section oc "Subdirectories. (DEPRECATED)";
+  List.iter (fprintf oc ".PHONY:%s\n") sds;
+  List.iter (fprintf oc "post-all::\n\tcd \"%s\" && $(MAKE) all\n") sds;
+  List.iter (fprintf oc "clean::\n\tcd \"%s\" && $(MAKE) clean\n") sds;
+  List.iter (fprintf oc "archclean::\n\tcd \"%s\" && $(MAKE) archclean\n") sds;
+  List.iter (fprintf oc "install-extra::\n\tcd \"%s\" && $(MAKE) install\n") sds
+   
+
+let generate_conf_includes oc { ml_includes; r_includes; q_includes } =
+  section oc "Path directives (-I, -R, -Q).";
+  let module S = String in
+  let open List in
+  let dash1 opt v = sprintf "-%s %s" opt (quote v) in
+  let dash2 opt v1 v2 = sprintf "-%s %s %s" opt (quote v1) (quote v2) in
+  fprintf oc "COQMF_OCAMLLIBS = %s\n"
+    (S.concat " " (map (fun { path } -> dash1 "I" path) ml_includes));
+  fprintf oc "COQMF_SRC_SUBDIRS = %s\n"
+    (S.concat " " (map (fun { path } -> quote path) ml_includes));
+  fprintf oc "COQMF_COQLIBS = %s %s %s\n"
+    (S.concat " " (map (fun { path } -> dash1 "I" path) ml_includes))
+    (S.concat " " (map (fun ({ path },l) -> dash2 "Q" path l) q_includes))
+    (S.concat " " (map (fun ({ path },l) -> dash2 "R" path l) r_includes));
+  fprintf oc "COQMF_COQLIBS_NOML = %s %s\n"
+    (S.concat " " (map (fun ({ path },l) -> dash2 "Q" path l) q_includes))
+    (S.concat " " (map (fun ({ path },l) -> dash2 "R" path l) r_includes))
+;;
+
+let generate_conf_coq_config oc args =
+  section oc "Coq configuration.";
+  Envars.print_config ~prefix_var_name:"COQMF_" oc;
+  fprintf oc "COQMF_MAKEFILE=%s\n" (quote (List.hd args)); 
+;;
+
+let generate_conf_files oc
+  { v_files; mli_files; ml4_files; ml_files; mllib_files; mlpack_files }
+=
+  let module S = String in
+  let open List in
+  section oc "Project files.";
+  fprintf oc "COQMF_VFILES = %s\n"      (S.concat " " (map quote v_files));
+  fprintf oc "COQMF_MLIFILES = %s\n"    (S.concat " " (map quote mli_files));
+  fprintf oc "COQMF_MLFILES = %s\n"     (S.concat " " (map quote ml_files));
+  fprintf oc "COQMF_ML4FILES = %s\n"    (S.concat " " (map quote ml4_files));
+  fprintf oc "COQMF_MLPACKFILES = %s\n" (S.concat " " (map quote mlpack_files));
+  fprintf oc "COQMF_MLLIBFILES = %s\n"  (S.concat " " (map quote mllib_files));
+;;
+
+let rec all_start_with prefix = function
+  | [] -> true
+  | [] :: _ -> false
+  | (x :: _) :: rest -> x = prefix && all_start_with prefix rest
+
+let rec logic_gcd acc = function
+  | [] -> acc
+  | [] :: _ -> acc
+  | (hd :: tl) :: rest ->
+      if all_start_with hd rest
+      then logic_gcd (acc @ [hd]) (tl :: List.map List.tl rest)
+      else acc
+
+let generate_conf_doc oc { defs; q_includes; r_includes } =
+  let includes = List.map snd (q_includes @ r_includes) in
+  let logpaths = List.map (CString.split '.') includes in
+  let gcd = logic_gcd [] logpaths in
+  let root =
+    if gcd = [] then
+      if not (List.mem_assoc "INSTALLDEFAULTROOT" defs) then begin
+         let destination = "orphan_" ^ (String.concat "_" includes) in
+         eprintf "Warning: no common logical root\n";
+         eprintf "Warning: in such case INSTALLDEFAULTROOT must be defined\n";
+         eprintf "Warning: the install-doc target is going to install files\n";
+         eprintf "Warning: in %s\n" destination;
+         destination
+      end else "$(INSTALLDEFAULTROOT)"
+    else String.concat "/" gcd in
+  Printf.fprintf oc "COQMF_INSTALLCOQDOCROOT = %s\n" (quote root)
+
+let generate_conf_defs oc { defs; extra_args } =
+  section oc "Extra variables.";
+  List.iter (fun (k,v) -> Printf.fprintf oc "%s = %s\n" k v) defs;
+  Printf.fprintf oc "COQMF_OTHERFLAGS = %s\n"
+    (String.concat " " extra_args)
+
+let generate_conf oc project args  =
+  fprintf oc "# This configuration file was generated by running:\n";
+  fprintf oc "# %s\n\n" (String.concat " " (List.map quote args));
+  generate_conf_files oc project;
+  generate_conf_includes oc project;
+  generate_conf_coq_config oc args;
+  generate_conf_defs oc project;
+  generate_conf_doc oc project;
+  generate_conf_extra_target oc project.extra_targets;
+  generate_conf_subdirs oc project.subdirs;
+;;
+
+let ensure_root_dir
+  ({ ml_includes; r_includes;
+     v_files; ml_files; mli_files; ml4_files;
+     mllib_files; mlpack_files } as project)
+=
+  let open List in
   let here = Sys.getcwd () in
-  let not_tops =  List.for_all (fun s -> s <> Filename.basename s) in
-  if List.exists (fun (_,_,x) -> x = here) i_inc
-    || List.exists (fun (_,_,x) -> is_prefix x here) r_inc
-    || (not_tops vfiles && not_tops mlis && not_tops ml4s && not_tops mls
-	&& not_tops mllibs && not_tops mlpacks)
+  let not_tops = List.for_all (fun s -> s <> Filename.basename s) in
+  if exists (fun { canonical_path = x } -> x = here) ml_includes
+  || exists (fun ({ canonical_path = x },_) -> is_prefix x here) r_includes
+  || (not_tops v_files &&
+      not_tops mli_files && not_tops ml4_files && not_tops ml_files &&
+      not_tops mllib_files && not_tops mlpack_files)
   then
-    inc
+    project
   else
-    ((".",here)::ml_inc,i_inc,(".","Top",here)::r_inc)
-
-let warn_install_at_root_directory (vfiles,(mlis,ml4s,mls,mllibs,mlpacks),_,_) inc =
-  let (inc_ml,inc_i,inc_r) = inc in
-  let inc_top = List.filter (fun (_,ldir,_) -> ldir = "") (inc_r@inc_i) in
-  let inc_top_p = List.map (fun (p,_,_) -> p) inc_top in
-  let files = vfiles @ mlis @ ml4s @ mls @ mllibs @ mlpacks in
-  if List.exists (fun f -> List.mem (Filename.dirname f) inc_top_p) files
-  then
-    Printf.eprintf "Warning: install target will copy files at the first level of the coq contributions installation directory; option -R or -Q %sis recommended\n"
-      (if inc_top = [] then "" else "with non trivial logical root ")
+    let here_path = { path = "."; canonical_path = here } in
+    { project with
+        ml_includes = here_path :: ml_includes;
+        r_includes = (here_path, "Top") :: r_includes }
+;;
+
+let warn_install_at_root_directory 
+  { q_includes; r_includes;
+    v_files; ml_files; mli_files; ml4_files;
+    mllib_files; mlpack_files }
+=
+  let open CList in
+  let inc_top_p =
+    map_filter
+      (fun ({ path } ,ldir) -> if ldir = "" then Some path else None)
+      (r_includes @ q_includes) in
+  let files =
+    v_files @ mli_files @ ml4_files @ ml_files @ mllib_files @ mlpack_files in
+  let bad = filter (fun f -> mem (Filename.dirname f) inc_top_p) files in
+  if bad <> [] then begin
+    eprintf "Warning: No file should be installed at the root of Coq's library.\n";
+    eprintf "Warning: No logical path (-R, -Q) applies to these files:\n";
+    List.iter (fun x -> eprintf "Warning:  %s\n" x) bad;
+    eprintf "\n";
+  end
+;;
 
-let check_overlapping_include (_,inc_i,inc_r) =
+let check_overlapping_include { q_includes; r_includes } =
   let pwd = Sys.getcwd () in
   let aux = function
     | [] -> ()
-    | (pdir,_,abspdir)::l ->
-	if not (is_prefix pwd abspdir) then
-	  Printf.eprintf "Warning: in option -R/-Q, %s is not a subdirectory of the current directory\n" pdir;
-	List.iter (fun (pdir',_,abspdir') ->
-	  if is_prefix abspdir abspdir' || is_prefix abspdir' abspdir then
-	    Printf.eprintf "Warning: in options -R/-Q, %s and %s overlap\n" pdir pdir') l;
-  in aux (inc_i@inc_r)
-
-(* Generate a .merlin file that references the standard library and
- * any -I included paths.
- *)
-let merlin targets (ml_inc,_,_) =
-  print ".merlin:\n";
-  print "\t@echo 'FLG -rectypes -safe-string' > .merlin\n" ;
-  List.iter (fun c ->
-      printf "\t@echo \"B $(COQLIB)%s\" >> .merlin\n" c)
-    lib_dirs ;
-  List.iter (fun (_,c) ->
-      printf "\t@echo \"B %s\" >> .merlin\n" c;
-      printf "\t@echo \"S %s\" >> .merlin\n" c)
-    ml_inc;
-  print "\n"
-
-let do_makefile args =
-  let has_file var = function
-    |[] -> var := false
-    |_::_ -> var := true in
-  let (project_file,makefile,is_install,opt),l =
-    try
-      Project_file.process_cmd_line Filename.current_dir_name
-       (None,None,Project_file.UnspecInstall,true) [] args
-    with Project_file.Parsing_error -> usage () in
-  let (v_f,(mli_f,ml4_f,ml_f,mllib_f,mlpack_f),sps,sds as targets), inc, defs =
-    Project_file.split_arguments l in
-
-  let () = match project_file with |None -> () |Some f -> make_name := f in
-  let () = match makefile with
-    |None -> ()
-    |Some f -> makefile_name := f; output_channel := open_out f in
-  has_file some_vfile v_f; has_file some_mlifile mli_f;
-  has_file some_mlfile ml_f; has_file some_ml4file ml4_f;
-  has_file some_mllibfile mllib_f; has_file some_mlpackfile mlpack_f;
-  let check_dep f =
-    if Filename.check_suffix f ".v" then some_vfile := true
-    else if (Filename.check_suffix f ".mli") then some_mlifile := true
-    else if (Filename.check_suffix f ".ml4") then some_ml4file := true
-    else if (Filename.check_suffix f ".ml") then some_mlfile := true
-    else if (Filename.check_suffix f ".mllib") then some_mllibfile := true
-    else if (Filename.check_suffix f ".mlpack") then some_mlpackfile := true
+    | ({ path; canonical_path }, _) :: l ->
+	if not (is_prefix pwd canonical_path) then
+	  eprintf "Warning: %s (used in -R or -Q) is not a subdirectory of the current directory\n\n" path;
+	List.iter (fun ({ path = p; canonical_path = cp }, _) ->
+	  if is_prefix canonical_path cp  || is_prefix cp canonical_path then
+	    eprintf "Warning: %s and %s overlap (used in -R or -Q)\n\n"
+              path p) l
   in
-  List.iter (fun (_,dependencies,_,_) ->
-    List.iter check_dep (Str.split (Str.regexp "[ \t]+") dependencies)) sps;
+    aux (q_includes @ r_includes)
+;;
+
+let chop_prefix p f =
+  let len_p = String.length p in
+  let len_f = String.length f in
+  String.sub f len_p (len_f - len_p)
+
+let clean_path p =
+  Str.global_replace (Str.regexp_string "//") "/" p
+
+let destination_of { ml_includes; q_includes; r_includes; } file =
+  let file_dir = CUnix.canonical_path_name (Filename.dirname file) in
+  let includes = q_includes @ r_includes in
+  let mk_destination logic canonical_path =
+    clean_path (physical_dir_of_logical_dir logic ^ "/" ^
+                chop_prefix canonical_path file_dir ^ "/") in
+  let candidates =
+    CList.map_filter (fun ({ canonical_path }, logic) ->
+      if is_prefix canonical_path file_dir then
+        Some(mk_destination logic canonical_path)
+      else None) includes
+  in
+  match candidates with
+  | [] ->
+     (* BACKWARD COMPATIBILITY: -I into the only logical root *)
+     begin match
+        r_includes,
+        List.find (fun { canonical_path = p } -> is_prefix p file_dir)
+          ml_includes
+     with
+        | [{ canonical_path }, logic], { canonical_path = p } ->
+            let destination =
+              clean_path (physical_dir_of_logical_dir logic ^ "/" ^
+                          chop_prefix p file_dir ^ "/") in
+            Printf.printf "%s" (quote destination)
+        | _ -> () (* skip *)
+        | exception Not_found -> () (* skip *)
+     end
+  | [s] -> Printf.printf "%s" (quote s)
+  | _ -> assert false
+
+let share_prefix s1 s2 =
+  let s1 = CString.split '.' s1 in
+  let s2 = CString.split '.' s2 in
+  match s1, s2 with
+  | x :: _ , y :: _ -> x = y
+  | _ -> false
+
+let _ =
+  let prog, args =
+    if Array.length Sys.argv = 1 then usage ();
+    let args = Array.to_list Sys.argv in
+    let prog = List.hd args in
+    prog, List.tl args in
 
-  let inc = ensure_root_dir targets inc in
-  if is_install <> Project_file.NoInstall then begin
-    warn_install_at_root_directory targets inc;
+  let only_destination, args = match args with
+    | "-destination-of" :: tgt :: rest -> Some tgt, rest
+    | _ -> None, args in
+
+  let project = 
+    try cmdline_args_to_project ~curdir:Filename.current_dir_name args
+    with Parsing_error s -> prerr_endline s; usage () in
+
+  if only_destination <> None then begin
+    destination_of project (Option.get only_destination);
+    exit 0
+  end;
+
+  if project.makefile = None then
+    eprintf "Warning: Omitting -o is deprecated\n\n";
+    (* We want to know the name of the Makefile (say m) in order to
+     * generate m.conf and include m.local *)
+
+  let conf_file = Option.default "CoqMakefile" project.makefile ^ ".conf" in
+  let local_file = Option.default "CoqMakefile" project.makefile ^ ".local" in
+
+  if project.extra_targets <> [] then begin
+    eprintf "Warning: -extra and -extra-phony are deprecated.\n";
+    eprintf "Warning: Write the extra targets in %s.\n\n" local_file;
+  end;
+
+  if project.subdirs <> [] then begin
+    eprintf "Warning: Subdirectories are deprecated.\n";
+    eprintf "Warning: Use double colon rules in %s.\n\n" local_file;
   end;
-  check_overlapping_include inc;
-  banner ();
-  header_includes ();
-  warning ();
-  command_line args;
-  parameters ();
-  include_dirs inc;
-  variables is_install opt defs;
-  all_target targets inc;
-  section "Special targets.";
-  standard opt;
-  install targets inc is_install;
-  merlin targets inc;
-  clean sds sps;
-  make_makefile sds;
-  implicit ();
-  warning ();
-  if not (makefile = None) then close_out !output_channel;
+
+  let project = ensure_root_dir project in
+  
+  if project.install_kind <> (Some CoqProject_file.NoInstall) then begin
+    warn_install_at_root_directory project;
+  end;
+
+  check_overlapping_include project;
+
+  Envars.set_coqlib ~fail:(fun x -> x);
+  
+  let ocm = Option.cata open_out stdout project.makefile in
+  generate_makefile ocm conf_file local_file (prog :: args) project;
+  close_out ocm;
+  let occ = open_out conf_file in
+  generate_conf occ project (prog :: args);
+  close_out occ;
   exit 0
 
-let _ =
-  let args =
-    if Array.length Sys.argv = 1 then usage ();
-    List.tl (Array.to_list Sys.argv)
-  in
-    do_makefile args
diff --git a/tools/coqc.ml b/tools/coqc.ml
index 552a943c8..9857d4318 100644
--- a/tools/coqc.ml
+++ b/tools/coqc.ml
@@ -83,8 +83,11 @@ let parse_args () =
 
     | ("-config" | "--config") :: _ ->
         Envars.set_coqlib ~fail:(fun x -> x);
-        Usage.print_config ();
+        Envars.print_config stdout;
         exit 0
+      
+    |"--print-version" :: _ ->
+        Usage.machine_readable_version 0
 
 (* Options for coqtop : a) options with 0 argument *)
 
diff --git a/tools/coqdep.ml b/tools/coqdep.ml
index 1c1c1be6a..930b092d3 100644
--- a/tools/coqdep.ml
+++ b/tools/coqdep.ml
@@ -435,7 +435,7 @@ let usage () =
      ML Module\" commands in coq files.\n";  *)
   (* Does not work anymore: *)
   (* eprintf " -D : Prints the missing ocmal module names. No dependency computed.\n"; *)
-  eprintf "  -boot : For coq developpers, prints dependencies over coq library files (omitted by default).\n";
+  eprintf "  -boot : For coq developers, prints dependencies over coq library files (omitted by default).\n";
   eprintf "  -sort : output the given file name ordered by dependencies\n";
   eprintf "  -noglob | -no-glob : \n";
   eprintf "  -I dir -as logname : add (non recursively) dir to coq load path under logical name logname\n";
diff --git a/tools/coqdep_common.ml b/tools/coqdep_common.ml
index 93b25e2ed..6e7935d09 100644
--- a/tools/coqdep_common.ml
+++ b/tools/coqdep_common.ml
@@ -219,7 +219,6 @@ let register_dir_logpath,find_dir_logpath =
 
 let file_name s = function
   | None     -> s
-  | Some "." -> s
   | Some d   -> d // s
 
 let depend_ML str =
@@ -293,15 +292,15 @@ let traite_fichier_modules md ext =
       (fun a_faire str -> match search_mlpack_known str with
 	| Some mldir ->
 	  let file = file_name str mldir in
-	  a_faire^" "^file
+          a_faire @ [file]
 	| None ->
 	  match search_ml_known str with
 	    | Some mldir ->
 	      let file = file_name str mldir in
-	      a_faire^" "^file
-	    | None -> a_faire) "" list
+              a_faire @ [file]
+            | None -> a_faire) [] list
   with
-    | Sys_error _ -> ""
+    | Sys_error _ -> []
     | Syntax_error (i,j) -> error_cannot_parse (md^ext) (i,j)
 
 (* Makefile's escaping rules are awful: $ is escaped by doubling and
@@ -443,7 +442,7 @@ let mL_dependencies () =
        let fullname = file_name name dirname in
        let dep = traite_fichier_modules fullname ".mllib" in
        let efullname = escape fullname in
-       printf "%s_MLLIB_DEPENDENCIES:=%s\n" efullname dep;
+       printf "%s_MLLIB_DEPENDENCIES:=%s\n" efullname (String.concat " " dep);
        printf "%s.cma:$(addsuffix .cmo,$(%s_MLLIB_DEPENDENCIES))\n" efullname efullname;
        printf "%s.cmxa:$(addsuffix .cmx,$(%s_MLLIB_DEPENDENCIES))\n" efullname efullname;
        flush stdout)
@@ -453,9 +452,13 @@ let mL_dependencies () =
        let fullname = file_name name dirname in
        let dep = traite_fichier_modules fullname ".mlpack" in
        let efullname = escape fullname in
-       printf "%s_MLPACK_DEPENDENCIES:=%s\n" efullname dep;
+       printf "%s_MLPACK_DEPENDENCIES:=%s\n" efullname (String.concat " " dep);
        printf "%s.cmo:$(addsuffix .cmo,$(%s_MLPACK_DEPENDENCIES))\n" efullname efullname;
        printf "%s.cmx:$(addsuffix .cmx,$(%s_MLPACK_DEPENDENCIES))\n" efullname efullname;
+       let efullname_capital = String.capitalize (Filename.basename efullname) in
+       List.iter (fun dep ->
+         printf "%s.cmx : FOR_PACK=-for-pack %s\n" dep efullname_capital)
+         dep;
        flush stdout)
     (List.rev !mlpackAccu)
 
diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml
index 2b9a04dad..8fca30268 100644
--- a/toplevel/coqinit.ml
+++ b/toplevel/coqinit.ml
@@ -121,14 +121,10 @@ let init_library_roots () =
    find the "include" file in the *source* directory *)
 let init_ocaml_path () =
   let add_subdir dl =
-    Mltop.add_ml_dir (List.fold_left (/) Envars.coqroot dl)
+    Mltop.add_ml_dir (List.fold_left (/) Envars.coqroot [dl])
   in
     Mltop.add_ml_dir (Envars.coqlib ());
-    List.iter add_subdir
-      [ [ "config" ]; [ "dev" ]; [ "lib" ]; [ "kernel" ]; [ "library" ];
-	[ "engine" ]; [ "pretyping" ]; [ "interp" ]; [ "parsing" ]; [ "proofs" ];
-	[ "tactics" ]; [ "toplevel" ]; [ "printing" ]; [ "intf" ];
-        [ "grammar" ]; [ "ide" ]; [ "ltac" ]; [ "vernac" ]; ]
+    List.iter add_subdir Envars.coq_src_subdirs
 
 let get_compat_version = function
   | "8.7" -> Flags.Current
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index dc0c2beba..fc05560f1 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -620,7 +620,7 @@ let init_toplevel arglist =
       Spawned.init_channels ();
       Envars.set_coqlib ~fail:CErrors.error;
       if !print_where then (print_endline(Envars.coqlib ()); exit(exitcode ()));
-      if !print_config then (Usage.print_config (); exit (exitcode ()));
+      if !print_config then (Envars.print_config stdout; exit (exitcode ()));
       if !print_tags then (print_style_tags (); exit (exitcode ()));
       if !filter_opts then (print_string (String.concat "\n" extras); exit 0);
       init_load_path ();
diff --git a/toplevel/usage.ml b/toplevel/usage.ml
index e29048035..c43f0ff05 100644
--- a/toplevel/usage.ml
+++ b/toplevel/usage.ml
@@ -56,7 +56,8 @@ let print_usage_channel co command =
 \n\
 \n  -where                 print Coq's standard library location and exit\
 \n  -config, --config      print Coq's configuration information and exit\
-\n  -v                     print Coq version and exit\
+\n  -v, --version          print Coq version and exit\
+\n  --print-version        print Coq version in easy to parse format and exit\
 \n  -list-tags             print highlight color tags known by Coq and exit\
 \n\
 \n  -quiet                 unset display of extra information (implies -w \"-all\")\
@@ -115,16 +116,3 @@ let print_usage_coqc () =
   flush stderr ;
   exit 1
 
-(* Print the configuration information *)
-
-let print_config () =
-  if Coq_config.local then Printf.printf "LOCAL=1\n" else Printf.printf "LOCAL=0\n";
-  Printf.printf "COQLIB=%s/\n" (Envars.coqlib ());
-  Printf.printf "DOCDIR=%s/\n" (Envars.docdir ());
-  Printf.printf "OCAMLFIND=%s\n" (Envars.ocamlfind ());
-  Printf.printf "CAMLP4=%s\n" Coq_config.camlp4;
-  Printf.printf "CAMLP4O=%s\n" Coq_config.camlp4o;
-  Printf.printf "CAMLP4BIN=%s/\n" (Envars.camlp4bin ());
-  Printf.printf "CAMLP4LIB=%s\n" (Envars.camlp4lib ());
-  Printf.printf "CAMLP4OPTIONS=%s\n" Coq_config.camlp4compat;
-  Printf.printf "HASNATDYNLINK=%s\n" (if Coq_config.has_natdynlink then "true" else "false")
diff --git a/toplevel/usage.mli b/toplevel/usage.mli
index dccb40e71..c46c7a79c 100644
--- a/toplevel/usage.mli
+++ b/toplevel/usage.mli
@@ -21,5 +21,3 @@ val add_to_usage : string -> string -> unit
 val print_usage_coqtop : unit -> unit
 val print_usage_coqc : unit -> unit
 
-(** {6 Prints the configuration information } *)
-val print_config : unit -> unit