Merge branch 'v8.5'

2 files changed, 103 insertions, 63 deletions

diff --git a/doc/refman/RefMan-syn.tex b/doc/refman/RefMan-syn.tex
index 37cbd1eac1..aabc8a8995 100644
--- a/doc/refman/RefMan-syn.tex
+++ b/doc/refman/RefMan-syn.tex
@@ -757,7 +757,8 @@ ways to change the interpretation of subterms are available.
 \subsubsection{Local opening of an interpretation scope 
 \label{scopechange}
 \index{\%}
-\comindex{Delimit Scope}}
+\comindex{Delimit Scope}
+\comindex{Undelimit Scope}}
 
 It is possible to locally extend the interpretation scope stack using
 the syntax ({\term})\%{\delimkey} (or simply {\term}\%{\delimkey}
@@ -774,6 +775,12 @@ To bind a delimiting key to a scope, use the command
 \texttt{Delimit Scope} {\scope} \texttt{with} {\ident} 
 \end{quote}
 
+To remove a delimiting key of a scope, use the command
+
+\begin{quote}
+\texttt{Undelimit Scope} {\scope}
+\end{quote}
+
 \subsubsection{Binding arguments of a constant to an interpretation scope
 \comindex{Arguments}}
 
diff --git a/doc/refman/RefMan-uti.tex b/doc/refman/RefMan-uti.tex
index 94290bc80f..0729391062 100644
--- a/doc/refman/RefMan-uti.tex
+++ b/doc/refman/RefMan-uti.tex
@@ -11,7 +11,7 @@ with {\ocaml} code statically linked, with the tool {\tt
   coqmktop}.
 
 For example, one can build a native-code \Coq\ toplevel extended with a tactic
-which source is in {\tt tactic.ml} with the command 
+which source is in {\tt tactic.ml} with the command
 \begin{verbatim}
      % coqmktop -opt -o mytop.out tactic.cmx
 \end{verbatim}
@@ -49,7 +49,7 @@ which detects the executables containing the word \texttt{coq}. In
 this case, the debugger is called with the required additional
 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. 
+subdirectory of the sources.
 
 \section[Modules dependencies]{Modules dependencies\label{Dependencies}\index{Dependencies}
   \ttindex{coqdep}}
@@ -74,76 +74,109 @@ 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}
+\section[Creating a {\tt Makefile} for \Coq\ modules]
+{Creating a {\tt Makefile} for \Coq\ modules
+\label{Makefile}
 \ttindex{Makefile}
-\ttindex{coq\_Makefile}}
-
-\paragraph{\_CoqProject}
-When a proof development becomes a larger project, split into several
-files or containing {\ocaml} plugins, files share common options that
-must be specified to all the executables used during the development
-of the project. It is therefore convenient to write a file that could
-be read all the components (the IDE, the compiler, etc.) that
-specify all the files and the common options of the project.
-
-An attempt to set up a format to write project files has been made
-from the command line option of the {\Coq} makefile generator
-\texttt{coq\_makefile}. It is described by \texttt{\% coq\_makefile
-  --help}. The default name for the project file understood by
-\texttt{coq\_makefile}, \texttt{coqide} and \texttt{Proof General} is
-\texttt{\_CoqProject}.
-
-A minimal usable project file can probably be obtained by the
-invocation
+\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.}
 
-While customizing a project file, mind the following requirements:
 \begin{itemize}
-\item {\Coq} files must end in \texttt{.v}, {\ocaml} modules in
-  \texttt{.ml4} if they require camlp preprocessing (and in
-  \texttt{.ml} otherwise), {\ocaml} module signatures, library
-  description and packing files respectively in \texttt{.mli},
-  \texttt{.mllib} and \texttt{.mlpack}.
-
-Any other argument that is not a valid option will be considered as a
-subdirectory. A specified subdirectory must have an inner
-\texttt{Makefile}. The phony targets \texttt{all} and \texttt{clean}
-will recursively call this target in all the subdirectories.
-
-\item \texttt{-R} and \texttt{-Q} options are for {\Coq}, \texttt{-I}
-  for {\ocaml}. The same directory may be ``included'' by both.
-
-  Using \texttt{-R} or \texttt{-Q} gives a correct logical path
-  and a correct installation location to your coq files.
-\item dependency on an external library must not be declared using a
-  \texttt{-Q \dots} in the \texttt{\_CoqProject} to include it in the
-  path, as the \textit{make clean} command would erase it! Instead,
-  install your dependency in a place automatically included by
-  {\Coq}. You can take advantage of the \texttt{COQPATH} variable
-  (see \ref{envars}) without installation if necessary.
-\item Use \texttt{-extra-phony} with no command to add an extra
+\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:
+  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}
 
-\paragraph{Coq\_makefile}
-The writing of a generic and complete \texttt{Makefile} may be tedious
-work and that's why {\Coq} provides a tool to automate its creation
-from the \texttt{\_CoqProject} file, \texttt{coq\_makefile}.
-
-Use
-\begin{quotation}
-\texttt{coq\_makefile -f \_CoqProject -o Makefile}
-\end{quotation}
-to generate a \texttt{Makefile} the first time. \texttt{Makefile} will be
-automatically regenerated when \texttt{\_CoqProject} is updated afterward.
 
 \section[Documenting \Coq\ files with coqdoc]{Documenting \Coq\ files with coqdoc\label{coqdoc}
 \ttindex{coqdoc}}
@@ -212,10 +245,10 @@ Instructions to use it are contained in this file.
 {\ProofGeneral} is a generic interface for proof assistants based on
 Emacs. The main idea is that the \Coq\ commands you are
 editing are sent to a \Coq\ toplevel running behind Emacs and the
-answers of the system automatically inserted into other Emacs buffers. 
+answers of the system automatically inserted into other Emacs buffers.
 Thus you don't need to copy-paste the \Coq\ material from your files
 to the \Coq\ toplevel or conversely from the \Coq\ toplevel to some
-files. 
+files.
 
 {\ProofGeneral} is developed and distributed independently of the
 system \Coq. It is freely available at \verb!proofgeneral.inf.ed.ac.uk!.
@@ -242,7 +275,7 @@ There are man pages for the commands {\tt coqdep}, {\tt gallina} and
 \RefManCutCommand{ENDREFMAN=\thepage}
 %END LATEX
 
-%%% Local Variables: 
+%%% Local Variables:
 %%% mode: latex
 %%% TeX-master: t
-%%% End: 
+%%% End: