Imported Upstream version 8.4~betaupstream/8.4_beta

26 files changed, 789 insertions, 495 deletions

diff --git a/doc/refman/Classes.tex b/doc/refman/Classes.tex
index f427609f..20ff649a 100644
--- a/doc/refman/Classes.tex
+++ b/doc/refman/Classes.tex
@@ -10,7 +10,7 @@
 \label{typeclasses}
 
 \begin{flushleft}
-  \em The status of Type Classes is experimental.
+  \em The status of Type Classes is (extremely) experimental.
 \end{flushleft}
 
 This chapter presents a quick reference of the commands related to type
@@ -128,7 +128,9 @@ particular support for type classes:
   methods. In the example above, \texttt{A} and \texttt{eqa} should be
   set maximally implicit.
 \item They support implicit quantification on partialy applied type
-  classes.
+  classes (\S \ref{implicit-generalization}).
+  Any argument not given as part of a type class binder will be
+  automatically generalized.
 \item They also support implicit quantification on superclasses
   (\S \ref{classes:superclasses})
 \end{itemize}
@@ -141,19 +143,6 @@ Definition neqb_impl `{eqa : EqDec A} (x y : A) := negb (eqb x y).
 Here \texttt{A} is implicitly generalized, and the resulting function
 is equivalent to the one above.
 
-The parsing of generalized type-class binders is different from regular
-binders:
-\begin{itemize}
-\item Implicit arguments of the class type are ignored.
-\item Superclasses arguments are automatically generalized.
-\item Any remaining arguments not given as part of a type class binder
-  will be automatically generalized. In other words, the rightmost
-  parameters are automatically generalized if not mentionned.
-\end{itemize}
-
-One can switch off this special treatment using the $!$ mark in front of
-the class name (see example below).
-
 \asection{Parameterized Instances}
 
 One can declare parameterized instances as in \Haskell simply by giving
@@ -242,9 +231,9 @@ Definition le_eqb `{Ord A} (x y : A) := andb (le x y) (le y x).
 \end{coq_example*}
 
 In some cases, to be able to specify sharing of structures, one may want to give
-explicitly the superclasses. It is possible to do it directly in regular
-generalized binders, and using the \texttt{!} modifier in class
-binders. For example:
+explicitly the superclasses. It is is possible to do it directly in regular
+binders, and using the \texttt{!} modifier in class binders. For
+example:
 \begin{coq_example*}
 Definition lt `{eqa : EqDec A, ! Ord eqa} (x y : A) := 
   andb (le x y) (neqb x y).
@@ -378,6 +367,12 @@ instances at the end of sections, or declaring structure projections as
 instances. This is almost equivalent to {\tt Hint Resolve {\ident} :
   typeclass\_instances}.
 
+\begin{Variants}
+\item {\tt Existing Instances {\ident}$_1$ \ldots {\ident}$_n$}
+  \comindex{Existing Instances}
+  With this command, several existing instances can be declared at once.
+\end{Variants}
+
 \subsection{\tt Context {\binder$_1$ \ldots \binder$_n$}}
 \comindex{Context}
 \label{Context}
diff --git a/doc/refman/Extraction.tex b/doc/refman/Extraction.tex
index cc9cf5c8..ee289ee7 100644
--- a/doc/refman/Extraction.tex
+++ b/doc/refman/Extraction.tex
@@ -469,9 +469,9 @@ mandatory. It only enhances readability of extracted code.
 You can then copy-paste the output to a file {\tt euclid.ml} or let 
 \Coq\ do it for you with the following command: 
 
-\begin{coq_example}
+\begin{verbatim}
 Extraction "euclid" eucl_dev.
-\end{coq_example}
+\end{verbatim}
 
 Let us play the resulting program:
 
@@ -543,8 +543,6 @@ Some pathological examples of extraction are grouped in the file
  After compilation those two examples run nonetheless,
  thanks to the correction of the extraction~\cite{Let02}. 
 
-% $Id: Extraction.tex 14575 2011-10-18 15:49:01Z letouzey $ 
-
 %%% Local Variables: 
 %%% mode: latex
 %%% TeX-master: "Reference-Manual"
diff --git a/doc/refman/Micromega.tex b/doc/refman/Micromega.tex
index 2fe7c2f7..5f9ed443 100644
--- a/doc/refman/Micromega.tex
+++ b/doc/refman/Micromega.tex
@@ -1,33 +1,24 @@
-\achapter{Micromega : tactics for solving arithmetics goals over ordered rings}
+\achapter{Micromega : tactics for solving arithmetic goals over ordered rings}
 \aauthor{Frédéric Besson and Evgeny Makarov}
 \newtheorem{theorem}{Theorem}
 
-For using the tactics out-of-the-box, read Section~\ref{sec:psatz-hurry}.
-%
-Section~\ref{sec:psatz-back} presents some background explaining the proof principle for solving polynomials goals.
-%
-Section~\ref{sec:lia} explains how to get a complete procedure for linear integer arithmetic.
-
-\asection{The {\tt psatz} tactic in a hurry}
-\tacindex{psatz}
+ 
+\asection{Short description of the tactics}
+\tacindex{psatz}  \tacindex{lra} 
 \label{sec:psatz-hurry}
-Load the {\tt Psatz} module ({\tt Require Psatz}.).  This module defines the tactics:
-{\tt lia}, {\tt psatzl D}, %{\tt sos D} 
-and {\tt psatz D n} where {\tt D} is {\tt Z}, {\tt Q} or {\tt R} and {\tt n} is an optional integer limiting the proof search depth.
-  % 
-  \begin{itemize}
-  \item The {\tt psatzl} tactic solves linear goals using an embedded (naive) linear programming prover \emph{i.e.},
-    fourier elimination.
-  \item The {\tt psatz} tactic solves polynomial goals using John Harrison's Hol light driver to the external prover {\tt cspd}\footnote{Sources and binaries can be found at \url{https://projects.coin-or.org/Csdp}}. Note that the {\tt csdp} driver is generating 
-    a \emph{proof cache} thus allowing to rerun scripts even without {\tt csdp}. 
-  \item The {\tt lia} (linear integer arithmetic) tactic is specialised to solve linear goals over $\mathbb{Z}$.
-    It extends {\tt psatzl Z} and exploits the discreetness of $\mathbb{Z}$.
-%%   \item The {\tt sos} tactic is another Hol light driver to the {\tt csdp} prover.  In theory, it is less general than
-%%     {\tt psatz}. In practice, even when {\tt psatz} fails, it can be worth a try -- see
-%%     Section~\ref{sec:psatz-back} for details.
-  \end{itemize}
-
-These tactics solve propositional formulas parameterised by atomic arithmetics expressions
+The {\tt Psatz} module ({\tt Require Psatz.}) gives access to several tactics for solving arithmetic goals over
+ {\tt Z}\footnote{Support for {\tt nat} and {\tt N} is obtained by pre-processing the goal with the {\tt zify} tactic.}, {\tt Q} and {\tt R}:
+\begin{itemize}
+\item {\tt lia} is a decision procedure for linear integer arithmetic (see Section~\ref{sec:lia});
+\item {\tt nia} is an incomplete proof procedure for integer non-linear arithmetic (see Section~\ref{sec:nia});
+\item {\tt lra} is a decision procedure for linear (real or rational) arithmetic goals (see Section~\ref{sec:lra});
+\item {\tt psatz D n} where {\tt D} is {\tt Z}, {\tt Q} or {\tt R} and {\tt n} is an optional integer limiting the proof search depth is
+is an incomplete proof procedure for non-linear arithmetic. It is based on John Harrison's Hol light driver to the external prover {\tt cspd}\footnote{Sources and binaries can be found at \url{https://projects.coin-or.org/Csdp}}. 
+   Note that the {\tt csdp} driver is generating 
+   a \emph{proof cache} thus allowing to rerun scripts even without {\tt csdp} (see Section~\ref{sec:psatz}). 
+\end{itemize}
+
+The tactics solve propositional formulas parameterised by atomic arithmetics expressions
 interpreted over a domain $D \in \{\mathbb{Z}, \mathbb{Q}, \mathbb{R} \}$.
 The syntax of the formulas is the following:
 \[
@@ -39,21 +30,29 @@ The syntax of the formulas is the following:
  \]
  where $c$ is a numeric constant, $x\in D$ is a numeric variable and the operators $-$, $+$, $\times$, are
  respectively subtraction, addition, product, $p \verb!^!n $ is exponentiation by a constant $n$, $P$ is an
- arbitrary proposition. %that is mostly ignored.
-%%
-%% Over $\mathbb{Z}$, $c$ is an integer ($c \in \mathtt{Z}$), over $\mathbb{Q}$, $c$ is 
-The following table details for each domain $D \in \{\mathbb{Z},\mathbb{Q},\mathbb{R}\}$ the range of constants $c$ and exponent $n$.
-\[
-\begin{array}{|c|c|c|c|}
-  \hline
-  &\mathbb{Z} & \mathbb{Q} & \mathbb{R} \\
-  \hline
-  c &\mathtt{Z} & \mathtt{Q} & \{R1, R0\} \\
-  \hline
-  n &\mathtt{Z} & \mathtt{Z} & \mathtt{nat}\\
-  \hline
-\end{array}
-\]
+ arbitrary proposition.
+ %
+ For {\tt Q}, equality is not leibnitz equality {\tt =} but the equality of rationals {\tt ==}.
+
+For {\tt Z} (resp. {\tt Q} ), $c$ ranges over integer constants (resp. rational constants).
+%% The following table details for each domain $D \in \{\mathbb{Z},\mathbb{Q},\mathbb{R}\}$ the range of constants $c$ and exponent $n$.
+%% \[
+%% \begin{array}{|c|c|c|c|}
+%%   \hline
+%%   &\mathbb{Z} & \mathbb{Q} & \mathbb{R} \\
+%%   \hline
+%%   c &\mathtt{Z} & \mathtt{Q} & (see below) \\
+%%   \hline
+%%   n &\mathtt{Z} & \mathtt{Z} & \mathtt{nat}\\
+%%   \hline
+%% \end{array}
+%% \]
+For {\tt R}, the tactic recognises as real constants the following expressions:
+\begin{verbatim}
+c ::= R0 | R1 | Rmul(c,c) | Rplus(c,c) | Rminus(c,c) | IZR z | IQR q | Rdiv(c,c) | Rinv c
+\end{verbatim}
+where ${\tt z}$ is a constant in {\tt Z} and {\tt q} is a constant in {\tt Q}.
+This includes integer constants written using the decimal notation \emph{i.e.,} {\tt c\%R}.
 
 \asection{\emph{Positivstellensatz} refutations}
 \label{sec:psatz-back}
@@ -87,6 +86,26 @@ For each conjunct $C_i$, the tactic calls a oracle which searches for $-1$ withi
 Upon success, the oracle returns a \emph{cone expression} that is normalised by the {\tt ring} tactic (see chapter~\ref{ring}) and checked to be
 $-1$.
 
+
+\asection{{\tt lra} : a decision procedure for linear real and rational arithmetic}
+\label{sec:lra}
+The {\tt lra} tactic is searching for \emph{linear} refutations using
+Fourier elimination\footnote{More efficient linear programming techniques could equally be employed}.  As a
+result, this tactic explores a subset of the $Cone$ defined as:
+\[
+LinCone(S) =\left\{ \left. \sum_{p \in S} \alpha_p \times p\ \right|\ \alpha_p \mbox{ are positive constants} \right\}
+\]
+The deductive power of {\tt lra} is the combined deductive power of {\tt ring\_simplify} and {\tt fourier}.
+%
+There is also an overlap with the {\tt field} tactic {\emph e.g.}, {\tt x = 10 * x / 10} is solved by {\tt lra}.
+
+\asection{ {\tt psatz} : a proof procedure for non-linear arithmetic}
+\label{sec:psatz}
+The {\tt psatz} tactic explores the $Cone$ by increasing degrees -- hence the depth parameter $n$.
+In theory, such a proof search is complete -- if the goal is provable the search eventually stops.
+Unfortunately, the external oracle is using numeric (approximate) optimisation techniques that might miss a
+refutation. 
+
 To illustrate the working of the tactic, consider we wish to prove the following Coq goal.\\
 \begin{coq_eval}
   Require Import ZArith Psatz.
@@ -104,30 +123,21 @@ expression belongs to $Cone(\{-x^2, x -1\})$.  Moreover, by running {\tt ring} w
 Theorem~\ref{thm:psatz}, the goal is valid.
 %
 
-\paragraph{The {\tt psatzl} tactic} is searching for \emph{linear} refutations using a fourier
-elimination\footnote{More efficient linear programming techniques could equally be employed}.
-As a result, this tactic explore a subset of the $Cone$  defined as:
-\[
-LinCone(S) =\left\{ \left. \sum_{p \in S} \alpha_p \times p\ \right|\ \alpha_p \mbox{ are positive constants} \right\}
-\]
-Basically, the deductive power of {\tt psatzl} is the combined deductive power of {\tt ring\_simplify} and {\tt fourier}.
-
-\paragraph{The {\tt psatz} tactic} explores the $Cone$ by increasing degrees -- hence the depth parameter $n$.
-In theory, such a proof search is complete -- if the goal is provable the search eventually stops.
-Unfortunately, the external oracle is using numeric (approximate) optimisation techniques that might miss a
-refutation. 
-
 %% \paragraph{The {\tt sos} tactic} -- where {\tt sos} stands for \emph{sum of squares} -- tries to prove that a
 %% single polynomial $p$ is positive by expressing it as a sum of squares \emph{i.e.,} $\sum_{i\in S} p_i^2$.
 %% This amounts to searching for $p$ in the cone without generators \emph{i.e.}, $Cone(\{\})$.
 %
 
-\asection{ {\tt lia} : the linear integer arithmetic tactic }
+\asection{ {\tt lia} : a tactic for linear integer arithmetic }
 \tacindex{lia}
 \label{sec:lia}
 
 The tactic {\tt lia} offers an alternative to the {\tt omega} and {\tt romega} tactic (see
-Chapter~\ref{OmegaChapter}). It solves goals that {\tt omega} and {\tt romega} do not solve, such as the
+Chapter~\ref{OmegaChapter}). 
+%
+Rougthly speaking, the deductive power of {\tt lia} is the combined deductive power of {\tt ring\_simplify} and {\tt omega}.
+%
+However, it solves linear goals that {\tt omega} and {\tt romega} do not solve, such as the
 following so-called \emph{omega nightmare}~\cite{TheOmegaPaper}.
 \begin{coq_example*}
   Goal forall x y, 
@@ -153,7 +163,7 @@ The canonical exemple is {\tt 2 * x = 1 -> False} which is a theorem of $\mathbb
 To remedy this weakness, the {\tt lia} tactic is using recursively a combination of:
 %
 \begin{itemize}
-\item linear \emph{positivstellensatz} refutations \emph{i.e.}, {\tt psatzl Z};
+\item linear \emph{positivstellensatz} refutations;
 \item cutting plane proofs;
 \item case split.
 \end{itemize}
@@ -189,7 +199,21 @@ Our current oracle tries to find an expression $e$ with a small range $[c_1,c_2]
 We generate $c_2 - c_1$ subgoals which contexts are enriched with an equation $e = i$ for $i \in [c_1,c_2]$ and
 recursively search for a proof.
 
-% This technique is used to solve so-called \emph{Omega nightmare}
+\asection{ {\tt nia} : a proof procedure for non-linear integer arithmetic}
+\tacindex{nia}
+\label{sec:nia}
+The {\tt nia} tactic is an {\emph experimental} proof procedure for non-linear  integer arithmetic.
+%
+The tactic performs a limited amount of non-linear reasoning before running the
+linear prover of {\tt lia}.
+This pre-processing does the following:
+\begin{itemize}
+\item If the context contains an arithmetic expression of the form $e[x^2]$ where $x$ is a
+  monomial, the context is enriched with $x^2\ge 0$;
+\item For all pairs of hypotheses $e_1\ge 0$, $e_2 \ge 0$, the context is enriched with $e_1 \times e_2 \ge 0$.
+\end{itemize}
+After pre-processing, the linear prover of {\tt lia} is searching for a proof by abstracting monomials by variables.
+
 
 
 %%% Local Variables: 
diff --git a/doc/refman/Nsatz.tex b/doc/refman/Nsatz.tex
index 794e461f..3ecc7e65 100644
--- a/doc/refman/Nsatz.tex
+++ b/doc/refman/Nsatz.tex
@@ -54,19 +54,17 @@ performed using {\em Type Classes}
 (see \ref{typeclasses})
 .
 
-The \texttt{Nsatz} module defines the generic tactic
-\texttt{nsatz}, which uses the low-level tactic \texttt{nsatz\_domainpv}: \\
+The \texttt{Nsatz} module defines the tactic
+\texttt{nsatz}, which can be used without arguments: \\
 \vspace*{3mm}
-\texttt{nsatz\_domainpv pretac rmax strategy lparam lvar simpltac domain}
-
+\texttt{nsatz}\\
+or with the syntax: \\
+\vspace*{3mm}
+\texttt{nsatz with radicalmax:={\em number}\%N strategy:={\em number}\%Z parameters:={\em list of variables} variables:={\em list of variables}}\\
 where:
 
 \begin{itemize}
-    \item \texttt{pretac} is a tactic depending on the ring A; its goal is to
-make apparent the generic operations of a domain (ring\_eq, ring\_plus, etc),
-both in the goal and the hypotheses; it is executed first. By default it is \texttt{ltac:idtac}.
-
-    \item \texttt{rmax} is a bound when for searching r s.t.$c (P-Q)^r =
+    \item \texttt{radicalmax} is a bound when for searching r s.t.$c (P-Q)^r =
 \sum_{i=1..s} S_i (P_i - Q_i)$
 	
     \item \texttt{strategy} gives the order on variables $X_1,...X_n$ and
@@ -80,7 +78,7 @@ the strategy used in Buchberger algorithm (see
 	        \item   strategy = 3: pure lexicographic order and sugar strategy.
 	\end{itemize}
 
-	\item \texttt{lparam} is the list of variables
+	\item \texttt{parameters} is the list of variables
 $X_{i_1},\ldots,X_{i_k}$  among $X_1,...,X_n$ which are considered as
    parameters: computation will be performed with rational fractions in these
    variables, i.e. polynomials are considered with coefficients in
@@ -88,21 +86,14 @@ $R(X_{i_1},\ldots,X_{i_k})$. In this case, the coefficient $c$ can be a non
 constant polynomial in $X_{i_1},\ldots,X_{i_k}$, and the tactic produces a goal
 which states that $c$ is not zero.
 
-	\item \texttt{lvar} is the list of the variables
-in the decreasing order in which they will be used in Buchberger algorithm. If \texttt{lvar} = {(@nil
+	\item \texttt{variables} is the list of the variables
+in the decreasing order in which they will be used in Buchberger algorithm. If \texttt{variables} = {(@nil
 R)}, then \texttt{lvar} is replaced by all the variables which are not in
-lparam.
-
-    \item \texttt{simpltac} is a tactic depending on the ring A; its goal is to
-simplify goals and make apparent the generic operations of a domain after
-simplifications. By default it is \texttt{ltac:simpl}.
-
- \item \texttt{domain} is the object of type Domain representing A, its
-operations and properties of integral domain.
+parameters.
 
 \end{itemize}
 
-See file \texttt{Nsatz.v} for examples.
+See file \texttt{Nsatz.v} for many examples, specially in geometry.
 
 %%% Local Variables: 
 %%% mode: latex
diff --git a/doc/refman/Program.tex b/doc/refman/Program.tex
index b41014ab..96073d71 100644
--- a/doc/refman/Program.tex
+++ b/doc/refman/Program.tex
@@ -3,11 +3,7 @@
 \aauthor{Matthieu Sozeau}
 \index{Program}
 
-\begin{flushleft}
-  \em The status of \Program\ is experimental.
-\end{flushleft}
-
-We present here the new \Program\ tactic commands, used to build certified
+We present here the \Program\ tactic commands, used to build certified
 \Coq\ programs, elaborating them from their algorithmic skeleton and a
 rich specification \cite{Sozeau06}. It can be sought of as a dual of extraction
 (see Chapter~\ref{Extraction}). The goal of \Program~is to program as in a regular
@@ -73,6 +69,8 @@ will be first rewrote to:
   works with the previous mechanism.
 \end{itemize}
 
+\subsection{Syntactic control over equalities}
+\label{ProgramSyntax}
 To give more control over the generation of equalities, the typechecker will
 fall back directly to \Coq's usual typing of dependent pattern-matching
 if a {\tt return} or {\tt in} clause is specified. Likewise,
@@ -89,9 +87,18 @@ Program Definition id (n : nat) : { x : nat | x = n } :=
   else S (pred n).
 \end{coq_example}
 
-Finally, the let tupling construct {\tt let (x1, ..., xn) := t in b}
+The let tupling construct {\tt let (x1, ..., xn) := t in b}
 does not produce an equality, contrary to the let pattern construct 
 {\tt let '(x1, ..., xn) := t in b}.
+Also, {\tt {\term}:>} explicitly asks the system to coerce {\tt \term} to its
+support type. It can be useful in notations, for example:
+\begin{coq_example}
+Notation " x `= y " := (@eq _ (x :>) (y :>)) (only parsing).
+\end{coq_example}
+
+This notation denotes equality on subset types using equality on their
+support types, avoiding uses of proof-irrelevance that would come up
+when reasoning with equality on the subset types themselves. 
 
 The next two commands are similar to their standard counterparts
 Definition (see Section~\ref{Basic-definitions}) and Fixpoint (see Section~\ref{Fixpoint}) in that
diff --git a/doc/refman/RefMan-add.tex b/doc/refman/RefMan-add.tex
index 9d7ca7b1..2094c9d2 100644
--- a/doc/refman/RefMan-add.tex
+++ b/doc/refman/RefMan-add.tex
@@ -51,8 +51,6 @@ can be found in the document {\tt Polynom.dvi}
 %anomalous behavior, please check first whether it has been already
 %reported in this document.
 
-% $Id: RefMan-add.tex 10061 2007-08-08 13:14:05Z msozeau $ 
-
 
 %%% Local Variables: 
 %%% mode: latex
diff --git a/doc/refman/RefMan-cic.tex b/doc/refman/RefMan-cic.tex
index dab164e7..9660a04b 100644
--- a/doc/refman/RefMan-cic.tex
+++ b/doc/refman/RefMan-cic.tex
@@ -1706,8 +1706,6 @@ impredicative system for sort \Set{} become~:
      
 
 
-% $Id: RefMan-cic.tex 13029 2010-05-28 11:49:12Z herbelin $ 
-
 %%% Local Variables: 
 %%% mode: latex
 %%% TeX-master: "Reference-Manual"
diff --git a/doc/refman/RefMan-coi.tex b/doc/refman/RefMan-coi.tex
index b0f0212e..619a8ee1 100644
--- a/doc/refman/RefMan-coi.tex
+++ b/doc/refman/RefMan-coi.tex
@@ -403,4 +403,3 @@ See \cite{Gimenez95b} for a complete description about this development.
 
 %\end{document}
 
-% $Id: RefMan-coi.tex 10421 2008-01-05 14:06:51Z herbelin $ 
diff --git a/doc/refman/RefMan-com.tex b/doc/refman/RefMan-com.tex
index 13a4219a..a40c210e 100644
--- a/doc/refman/RefMan-com.tex
+++ b/doc/refman/RefMan-com.tex
@@ -34,11 +34,6 @@ toplevel (to allow the dynamic link of tactics).  You can switch to
 the Caml toplevel with the command \verb!Drop.!, and come back to the
 \Coq~toplevel with the command \verb!Toplevel.loop();;!.
 
-% The command \verb!coqtop -searchisos! runs the search tool {\sf
-%   Coq\_SearchIsos} (see Section~\ref{coqsearchisos},
-% page~\pageref{coqsearchisos}) and, as the \Coq~system, can be combined
-% with the option \verb!-opt!.
-
 \section{Batch compilation ({\tt coqc})}
 The {\tt coqc} command takes a name {\em file} as argument.  Then it
 looks for a vernacular file named {\em file}{\tt .v}, and tries to
@@ -58,12 +53,15 @@ native-code versions of the system.
 \section[Resource file]{Resource file\index{Resource file}}
 
 When \Coq\ is launched, with either {\tt coqtop} or {\tt coqc}, the
-resource file \verb:$HOME/.coqrc.7.0: is loaded, where \verb:$HOME: is
-the home directory of the user.  If this file is not found, then the
-file \verb:$HOME/.coqrc: is searched. You can also specify an
+resource file \verb:$XDG_CONFIG_HOME/coq/coqrc.xxx: is loaded, where
+\verb:$XDG_CONFIG_HOME: is the configuration directory of the user (by
+default its home directory \verb!/.config! and \verb:xxx: is the version
+number (e.g. 8.3).  If this file is not found, then the file
+\verb:$XDG_CONFIG_HOME/coqrc: is searched. You can also specify an
 arbitrary name for the resource file (see option \verb:-init-file:
-below), or the name of another user to load the resource file of
-someone else (see option \verb:-user:).
+below), or the name of another user to load the resource file of someone
+else (see option \verb:-user:).
+
 
 This file may contain, for instance, \verb:Add LoadPath: commands to add
 directories to the load path of \Coq.
@@ -73,9 +71,11 @@ option \verb:-q:.
 \section[Environment variables]{Environment variables\label{EnvVariables}
 \index{Environment variables}}
 
-There are three environment variables used by the \Coq\ system.
+There are four environment variables used by the \Coq\ system.
 \verb:$COQBIN: for the directory where the binaries are,
-\verb:$COQLIB: for the directory where the standard library is, and 
+\verb:$COQLIB: for the directory where the standard library is,
+\verb:$COQPATH: for a list of directories seperated by \verb|:|
+(\verb|;| on windows) to add to the load path, and
 \verb:$COQTOP: for the directory of the sources. The latter is useful
 only for developers that are writing their own tactics and are using
 \texttt{coq\_makefile} (see \ref{Makefile}). If \verb:$COQBIN: or
@@ -83,6 +83,11 @@ only for developers that are writing their own tactics and are using
 (defined at installation time). So these variables are useful only if
 you move the \Coq\ binaries and library after installation.
 
+Coq will also honor \verb:$XDG_DATA_HOME: and \verb:$XDG_DATA_DIRS: (see
+\url{http://standards.freedesktop.org/basedir-spec/basedir-spec-latest.html}).
+Coq adds \verb:${XDG_DATA_HOME}/coq: and \verb:${XDG_DATA_DIRS}/coq: to its
+search path.
+
 \section[Options]{Options\index{Options of the command line}
 \label{vmoption}
 \label{coqoptions}}
@@ -173,11 +178,6 @@ The following command-line options are recognized by the commands {\tt
 
   Cause \Coq~not to load the resource file.
 
-\item[{\tt -user} {\em username}]\ 
-
-  Take resource file of user {\em username} (that is 
-  \verb+~+{\em username}{\tt /.coqrc.7.0}) instead of yours.
-
 \item[{\tt -load-ml-source} {\em file}]\ 
 
   Load the Caml source file {\em file}.
@@ -263,9 +263,25 @@ The following command-line options are recognized by the commands {\tt
  
 \item[{\tt -dont-load-proofs}]\ 
 
-  This avoids loading in memory the proofs of opaque theorems
-  resulting in a smaller memory requirement and faster compilation;
-  warning: this invalidates some features such as the extraction tool.
+  Warning: this is an unsafe mode.
+  Instead of loading in memory the proofs of opaque theorems, they are
+  treated as axioms. This results in smaller memory requirement and
+  faster compilation, but the behavior of the system might slightly change
+  (for instance during module subtyping), and some features won't be
+  available (for example {\tt Print Assumptions}).
+
+\item[{\tt -lazy-load-proofs}]\
+
+  This is the default behavior. Proofs of opaque theorems aren't
+  loaded immediately in memory, but only when necessary, for instance
+  during some module subtyping or {\tt Print Assumptions}. This should be
+  almost as fast and efficient as {\tt -dont-load-proofs}, with none
+  of its drawbacks.
+
+\item[{\tt -force-load-proofs}]\
+
+  Proofs of opaque theorems are loaded in memory as soon as the
+  corresponding {\tt Require} is done. This used to be Coq's default behavior.
 
 \item[{\tt -vm}]\ 
 
@@ -376,8 +392,6 @@ makes more disk access. It is also less secure since an attacker might
 have replaced the compiled library $A$ after it has been read by the
 first command, but before it has been read by the second command.
 
-% $Id: RefMan-com.tex 12443 2009-10-29 16:17:29Z gmelquio $ 
-
 %%% Local Variables: 
 %%% mode: latex
 %%% TeX-master: "Reference-Manual"
diff --git a/doc/refman/RefMan-ext.tex b/doc/refman/RefMan-ext.tex
index c0e578fe..2da5bec1 100644
--- a/doc/refman/RefMan-ext.tex
+++ b/doc/refman/RefMan-ext.tex
@@ -200,6 +200,20 @@ Definition b := {| x := 5; y := 3 |}.
 Definition c := {| y := 3; x := 5 |}.
 \end{coq_example}
 
+This syntax can be disabled globally for printing by
+\begin{quote}
+{\tt Unset Printing Records.}
+\end{quote}
+For a given type, one can override this using either
+\begin{quote}
+{\tt Add Printing Record {\ident}.}
+\end{quote}
+to get record syntax or
+\begin{quote}
+{\tt Add Printing Constructor {\ident}.}
+\end{quote}
+to get constructor syntax.
+
 This syntax can also be used for pattern matching.
 
 \begin{coq_example}
@@ -675,7 +689,15 @@ Function plus (n m : nat) {struct n} : nat :=
 \paragraph[Limitations]{Limitations\label{sec:Function-limitations}}
 \term$_0$ must be build as a \emph{pure pattern-matching tree}
 (\texttt{match...with}) with applications only \emph{at the end} of
-each branch.  For now dependent cases are not treated.
+each branch.  
+
+Function does not support partial application of the function being defined. Thus, the following example cannot be accepted due to the presence of partial application of \ident{wrong} into the body of \ident{wrong}~:
+\begin{coq_example*}
+  Function wrong (C:nat) {\ldots} : nat := 
+    List.hd(List.map wrong (C::nil)).
+\end{coq_example*}
+
+For now dependent cases are not treated for non structurally terminating functions.
 
 
 
@@ -1119,14 +1141,14 @@ possible, the correct argument will be automatically generated.
 \end{ErrMsgs}
 
 \subsection{Declaration of implicit arguments for a constant
-\comindex{Implicit Arguments}}
+\comindex{Arguments}}
 \label{ImplicitArguments}
 
 In case one wants that some arguments of a given object (constant,
 inductive types, constructors, assumptions, local or not) are always
 inferred by Coq, one may declare once and for all which are the expected
 implicit arguments of this object. There are two ways to do this,
-a-priori and a-posteriori. 
+a priori and a posteriori.
 
 \subsubsection{Implicit Argument Binders}
 
@@ -1166,44 +1188,44 @@ Print list.
 One can always specify the parameter if it is not uniform using the
 usual implicit arguments disambiguation syntax.
 
-\subsubsection{The Implicit Arguments Vernacular Command}
+\subsubsection{Declaring Implicit Arguments}
 
-To set implicit arguments for a constant a-posteriori, one can use the
+To set implicit arguments for a constant a posteriori, one can use the
 command:
 \begin{quote}
-\tt Implicit Arguments {\qualid} [ \nelist{\possiblybracketedident}{} ]
+\tt Arguments {\qualid} \nelist{\possiblybracketedident}{}
 \end{quote}
-where the list of {\possiblybracketedident} is the list of parameters
-to be declared implicit, each of the identifier of the list being
-optionally surrounded by square brackets, then meaning that this
-parameter has to be maximally inserted.
+where the list of {\possiblybracketedident} is the list of all arguments of
+{\qualid} where the ones to be declared implicit are surrounded by
+square brackets and the ones to be declared as maximally inserted implicits
+are surrounded by curly braces.
 
 After the above declaration is issued, implicit arguments can just (and
 have to) be skipped in any expression involving an application of
 {\qualid}.
 
 \begin{Variants}
-\item {\tt Global Implicit Arguments {\qualid} [ \nelist{\possiblybracketedident}{} ]
-\comindex{Global Implicit Arguments}}
+\item {\tt Global Arguments {\qualid} \nelist{\possiblybracketedident}{}
+\comindex{Global Arguments}}
 
-Tells to recompute the implicit arguments of {\qualid} after ending of
+Tell to recompute the implicit arguments of {\qualid} after ending of
 the current section if any, enforcing the implicit arguments known
 from inside the section to be the ones declared by the command.
 
-\item {\tt Local Implicit Arguments {\qualid} [ \nelist{\possiblybracketedident}{} ]
-\comindex{Local Implicit Arguments}}
+\item {\tt Local Arguments {\qualid} \nelist{\possiblybracketedident}{}
+\comindex{Local Arguments}}
 
-When in a module, tells not to activate the implicit arguments of
-{\qualid} declared by this commands to contexts that requires the
+When in a module, tell not to activate the implicit arguments of
+{\qualid} declared by this command to contexts that require the
 module.
 
-\item {\tt \zeroone{Global {\sl |} Local} Implicit Arguments {\qualid} \sequence{[ \nelist{\possiblybracketedident}{} ]}{}}
+\item {\tt \zeroone{Global {\sl |} Local} Arguments {\qualid} \sequence{\nelist{\possiblybracketedident}{}}{,}}
 
 For names of constants, inductive types, constructors, lemmas which
 can only be applied to a fixed number of arguments (this excludes for
-instance constants whose type is polymorphic), multiple lists
-of implicit arguments can be given. These lists must be of different
-length, and, depending on the number of arguments {\qualid} is applied
+instance constants whose type is polymorphic), multiple 
+implicit arguments decflarations can be given. 
+Depending on the number of arguments {\qualid} is applied
 to in practice, the longest applicable list of implicit arguments is
 used to select which implicit arguments are inserted.
 
@@ -1223,17 +1245,17 @@ Inductive list (A:Type) : Type :=
 \end{coq_example*}
 \begin{coq_example}
 Check (cons nat 3 (nil nat)).
-Implicit Arguments cons [A].
-Implicit Arguments nil [A].
+Arguments cons [A] _ _.
+Arguments nil [A].
 Check (cons 3 nil).
 Fixpoint map (A B:Type) (f:A->B) (l:list A) : list B :=
   match l with nil => nil | cons a t => cons (f a) (map A B f t) end.
 Fixpoint length (A:Type) (l:list A) : nat :=
   match l with nil => 0 | cons _ m => S (length A m) end.
-Implicit Arguments map [A B].
-Implicit Arguments length [[A]]. (* A has to be maximally inserted *)
+Arguments map [A B] f l.
+Arguments length {A} l. (* A has to be maximally inserted *)
 Check (fun l:list (list nat) => map length l).
-Implicit Arguments map [A B] [A] [].
+Arguments map [A B] f l, [A] B f l, A B f l.
 Check (fun l => map length l = map (list nat) nat length l).
 \end{coq_example}
 
@@ -1248,8 +1270,8 @@ implicit arguments of {\qualid}.
 {\Coq} can also automatically detect what are the implicit arguments
 of a defined object. The command is just
 \begin{quote}
-{\tt Implicit Arguments {\qualid}
-\comindex{Implicit Arguments}}
+{\tt Arguments {\qualid} : default implicits
+\comindex{Arguments}}
 \end{quote}
 The auto-detection is governed by options telling if strict,
 contextual, or reversible-pattern implicit arguments must be
@@ -1258,16 +1280,16 @@ Sections~\ref{SetStrictImplicit},~\ref{SetContextualImplicit},~\ref{SetReversibl
 and also~\ref{SetMaximalImplicitInsertion}).
 
 \begin{Variants}
-\item {\tt Global Implicit Arguments {\qualid}
-\comindex{Global Implicit Arguments}}
+\item {\tt Global Arguments {\qualid} : default implicits
+\comindex{Global Arguments}}
 
-Tells to recompute the implicit arguments of {\qualid} after ending of
+Tell to recompute the implicit arguments of {\qualid} after ending of
 the current section if any.
 
-\item {\tt Local Implicit Arguments {\qualid}
-\comindex{Local Implicit Arguments}}
+\item {\tt Local Arguments {\qualid} : default implicits
+\comindex{Local Arguments}}
 
-When in a module, tells not to activate the implicit arguments of
+When in a module, tell not to activate the implicit arguments of
 {\qualid} computed by this declaration to contexts that requires the
 module.
 
@@ -1283,12 +1305,12 @@ Inductive list (A:Set) : Set :=
   | cons : A -> list A -> list A.
 \end{coq_example*}
 \begin{coq_example}
-Implicit Arguments cons.
+Arguments cons : default implicits.
 Print Implicit cons.
-Implicit Arguments nil.
+Arguments nil : default implicits.
 Print Implicit nil.
 Set Contextual Implicit.
-Implicit Arguments nil.
+Arguments nil : default implicits.
 Print Implicit nil.
 \end{coq_example}
 
@@ -1304,7 +1326,7 @@ Definition Relation := X -> X -> Prop.
 Definition Transitivity (R:Relation) :=
   forall x y:X, R x y -> forall z:X, R y z -> R x z.
 Variables (R : Relation) (p : Transitivity R).
-Implicit Arguments p.
+Arguments p : default implicits.
 \end{coq_example*}
 \begin{coq_example}
 Print p.
@@ -1317,6 +1339,21 @@ Variables (a b c : X) (r1 : R a b) (r2 : R b c).
 Check (p r1 r2).
 \end{coq_example}
 
+Implicit arguments can be cleared with the following syntax:
+
+\begin{quote}
+{\tt Arguments {\qualid} : clear implicits
+\comindex{Arguments}}
+\end{quote}
+
+In the following example implict arguments declarations for the {\tt nil}
+constant are cleared:
+\begin{coq_example}
+Arguments cons : clear implicits.
+Print Implicit cons.
+\end{coq_example}
+
+
 \subsection{Mode for automatic declaration of implicit arguments
 \label{Auto-implicit}
 \comindex{Set Implicit Arguments}
@@ -1410,7 +1447,7 @@ Implicit Insertion}.
 \subsection{Explicit applications
 \index{Explicitly given implicit arguments}
 \label{Implicits-explicitation}
-\index{qualid@{\qualid}}}
+\index{qualid@{\qualid}} \index{\symbol{64}}}
 
 In presence of non strict or contextual argument, or in presence of
 partial applications, the synthesis of implicit arguments may fail, so
@@ -1442,6 +1479,28 @@ Check (p r1 (z:=c)).
 Check (p (x:=a) (y:=b) r1 (z:=c) r2).
 \end{coq_example}
 
+\subsection{Renaming implicit arguments
+\comindex{Arguments}
+}
+
+Implicit arguments names can be redefined using the following syntax:
+\begin{quote}
+{\tt Arguments {\qualid} \nelist{\name}{}  : rename}
+\end{quote}
+
+Without the {\tt rename} flag, {\tt Arguments} can be used to assert
+that a given constant has the expected number of arguments and that
+these arguments are named as expected.
+
+\noindent {\bf Example (continued): }
+\begin{coq_example}
+Arguments p [s t] _ [u] _: rename.
+Check (p r1 (u:=c)).
+Check (p (s:=a) (t:=b) r1 (u:=c) r2).
+Fail Arguments p [s t] _ [w] _.
+\end{coq_example}
+
+
 \subsection{Displaying what the implicit arguments are
 \comindex{Print Implicit}
 \label{PrintImplicit}}
@@ -1622,7 +1681,7 @@ the generalized variables. Inside implicit generalization
 delimiters, free variables in the current context are automatically
 quantified using a product or a lambda abstraction to generate a closed
 term. In the following statement for example, the variables \texttt{n}
-and \texttt{m} are automatically generalized and become explicit
+and \texttt{m} are autamatically generalized and become explicit
 arguments of the lemma as we are using \verb|`( )|:
 
 \begin{coq_example}
@@ -1638,7 +1697,7 @@ generalizations when mistyping identifiers. There are three variants of
 the command:
 
 \begin{quote}
-{\tt (Global)? Generalizable (All|No) Variable(s)? ({\ident$_1$ \ident$_n$})?.}
+{\tt Generalizable (All|No) Variable(s)? ({\ident$_1$ \ident$_n$})?.}
 \end{quote}
 
 \begin{Variants}
@@ -1742,13 +1801,25 @@ of the occurrences of {\Type}, use
 \end{quote}
 
 \comindex{Print Universes}
+\comindex{Print Sorted Universes}
 
 The constraints on the internal level of the occurrences of {\Type}
 (see Section~\ref{Sorts}) can be printed using the command
 \begin{quote}
-{\tt Print Universes.}
+{\tt Print \zeroone{Sorted} Universes.}
 \end{quote}
+If the optional {\tt Sorted} option is given, each universe will be
+made equivalent to a numbered label reflecting its level (with a
+linear ordering) in the universe hierarchy.
 
+This command also accepts an optional output filename:
+\begin{quote}
+\tt Print \zeroone{Sorted} Universes {\str}.
+\end{quote}
+If {\str} ends in \texttt{.dot} or \texttt{.gv}, the constraints are
+printed in the DOT language, and can be processed by Graphviz
+tools. The format is unspecified if {\str} doesn't end in
+\texttt{.dot} or \texttt{.gv}.
 
 %%% Local Variables: 
 %%% mode: latex
diff --git a/doc/refman/RefMan-gal.tex b/doc/refman/RefMan-gal.tex
index d1489591..204fa90d 100644
--- a/doc/refman/RefMan-gal.tex
+++ b/doc/refman/RefMan-gal.tex
@@ -217,12 +217,12 @@ possible one (among all tokens defined at this moment), and so on.
 
 \subsection{Syntax of terms}
 
-Figures \ref{term-syntax} and \ref{term-syntax-aux} describe the basic
-set of terms which form the {\em Calculus of Inductive Constructions}
-(also called \CIC). The formal presentation of {\CIC} is given in
-Chapter \ref{Cic}. Extensions of this syntax are given in chapter
-\ref{Gallina-extension}. How to customize the syntax is described in
-Chapter \ref{Addoc-syntax}.
+Figures \ref{term-syntax} and \ref{term-syntax-aux} describe the basic syntax of
+the terms of the {\em Calculus of Inductive Constructions} (also
+called \CIC). The formal presentation of {\CIC} is given in Chapter
+\ref{Cic}. Extensions of this syntax are given in chapter
+\ref{Gallina-extension}. How to customize the syntax is described in Chapter
+\ref{Addoc-syntax}.
 
 \begin{figure}[htbp]
 \begin{centerframe}
@@ -240,9 +240,13 @@ Chapter \ref{Addoc-syntax}.
  & $|$ & {\tt let} {\tt (} \sequence{\name}{,} {\tt )} \zeroone{\ifitem}
          {\tt :=} {\term}
          {\tt in} {\term}  &(\ref{caseanalysis}, \ref{Mult-match})\\
+ & $|$ & {\tt let '} {\pattern} \zeroone{{\tt in} {\term}} {\tt :=} {\term}
+        \zeroone{\returntype} {\tt in} {\term} & (\ref{caseanalysis}, \ref{Mult-match})\\
  & $|$ & {\tt if} {\term} \zeroone{\ifitem} {\tt then} {\term}
          {\tt else} {\term} &(\ref{caseanalysis}, \ref{Mult-match})\\
  & $|$ & {\term} {\tt :} {\term} &(\ref{typecast})\\
+ & $|$ & {\term} {\tt <:} {\term} &(\ref{typecast})\\
+ & $|$ & {\term} {\tt :>} &(\ref{ProgramSyntax})\\
  & $|$ & {\term} {\tt ->} {\term} &(\ref{products})\\
  & $|$ & {\term} \nelist{\termarg}{}&(\ref{applications})\\
  & $|$ & {\tt @} {\qualid} \sequence{\term}{}
@@ -256,6 +260,7 @@ Chapter \ref{Addoc-syntax}.
  & $|$ & {\sort} &(\ref{Gallina-sorts})\\
  & $|$ & {\num} &(\ref{numerals})\\
  & $|$ & {\_} &(\ref{hole})\\
+ & $|$ & {\tt (} {\term} {\tt )} & \\
  & & &\\
 {\termarg} & ::= & {\term} &\\
  & $|$ & {\tt (} {\ident} {\tt :=} {\term} {\tt )}
@@ -496,6 +501,10 @@ arguments is used for making explicit the value of implicit arguments
 The expression ``{\term}~{\tt :}~{\type}'' is a type cast
 expression. It enforces the type of {\term} to be {\type}.
 
+``{\term}~{\tt <:}~{\type}'' locally sets up the virtual machine (as if option
+{\tt Virtual Machine} were on, see \ref{SetVirtualMachine}) for checking that
+{\term} has type {\type}.
+
 \subsection{Inferable subterms
 \label{hole}
 \index{\_}}
diff --git a/doc/refman/RefMan-ide.tex b/doc/refman/RefMan-ide.tex
index 5d9c8c16..f061ef18 100644
--- a/doc/refman/RefMan-ide.tex
+++ b/doc/refman/RefMan-ide.tex
@@ -261,32 +261,26 @@ CONTROL and the SHIFT keys, and type the hexadecimal code of the
 symbol required, for example \verb|2200| for the $\forall$ symbol.
 A list of symbol codes is available at \url{http://www.unicode.org}. 
 
-This method obviously doesn't scale, that's why the preferred
-alternative is to use an Input Method Editor. On POSIX systems (Linux
-distributions, BSD variants and MacOS X), you can use \texttt{uim} to
-support \LaTeX{}-style edition and, if using X Windows, you can also use
-the XCompose method (XIM). How to use \texttt{uim} is documented below.
-
-If you have \texttt{uim} 1.5.x, first manually copy the files located
-in directory {\tt ide/uim} of the Coq source distribution to the
-{\tt uim} directory of input methods which typically is {\tt
-  /usr/share/uim}. Execute {\tt uim-module-manager -{-}register
-  coqide}. Then, execute \texttt{uim-pref-gtk} as regular user and set
-the default Input Method to "CoqIDE" in the "Global Settings" group
-(don't forget to tick the checkbox "Specify default IM"; you may also
-have to first edit the set of "Enabled input method" to add CoqIDE to
-the set). You can now execute CoqIDE with the following commands
-(assuming you use a Bourne-style shell):
+This method obviously doesn't scale, that's why the preferred alternative is to
+use an Input Method Editor. On POSIX systems (Linux distros, BSD variants and
+MacOS X), you can use \texttt{uim} version 1.6 or later which provides a \LaTeX{}-style
+input method.
+
+To configure \texttt{uim}, execute \texttt{uim-pref-gtk} as your regular user.
+In the "Global Settings" group set the default Input Method to "ELatin" (don't
+forget to tick the checkbox "Specify default IM"). In the "ELatin" group set the
+layout to "TeX", and remember the content of the "[ELatin] on" field (by default
+"<Control>\textbackslash"). You can now execute CoqIDE with the following commands (assuming
+you use a Bourne-style shell):
 
 \begin{verbatim}
 $ export GTK_IM_MODULE=uim
 $ coqide
 \end{verbatim}
 
-If you then type the sequence "\verb=\Gamma=", you will see the sequence being
-replaced by $\Gamma$ as soon as you  type the second "a".
-
-If you have \texttt{uim} 1.6.x, the \LaTeX{} input method is built-in. You just have to execute \texttt{uim-pref-gtk} and choose "ELatin" as default Input Method in the "Global Settings". Then, in the "ELatin" group set the layout to "TeX", and remember the content of the "[ELatin] on" field (by default "<Control>$\backslash$"). Proceed then as above.
+Activate the ELatin Input Method with Ctrl-\textbackslash, then type the
+sequence "\verb=\Gamma=". You will see the sequence being
+replaced by $\Gamma$ as soon as you type the second "a".
 
 \subsection[Character encoding for saved files]{Character encoding for saved files\label{sec:coqidecharencoding}}
 
@@ -305,23 +299,6 @@ each dot is an hexadecimal digit: the number between braces is the
 hexadecimal UNICODE index for the missing character.
 
 
-\section{Building a custom \CoqIDE{} with user \textsc{ML} code}
-
-You can do this as described in Section~\ref{Coqmktop} for a
-custom coq text toplevel, simply by adding 
-option \verb|-ide| to \verb|coqmktop|, that is something like
-\begin{quote}
-\texttt{coqmktop -ide -byte $m_1$.cmo \ldots{} $m_n$.cmo}
-\end{quote}
-or 
-\begin{quote}
-\texttt{coqmktop -ide -opt $m_1$.cmx \ldots{} $m_n$.cmx}
-\end{quote}
-
-    
-
-% $Id: RefMan-ide.tex 13701 2010-12-10 07:48:30Z herbelin $ 
-
 %%% Local Variables: 
 %%% mode: latex
 %%% TeX-master: "Reference-Manual"
diff --git a/doc/refman/RefMan-ind.tex b/doc/refman/RefMan-ind.tex
index af4257ca..95944240 100644
--- a/doc/refman/RefMan-ind.tex
+++ b/doc/refman/RefMan-ind.tex
@@ -508,4 +508,3 @@ Check tree_forest_mutind.
 
 %\end{document}
 
-% $Id: RefMan-ind.tex 10421 2008-01-05 14:06:51Z herbelin $ 
diff --git a/doc/refman/RefMan-int.tex b/doc/refman/RefMan-int.tex
index 7b531409..6d2c37f7 100644
--- a/doc/refman/RefMan-int.tex
+++ b/doc/refman/RefMan-int.tex
@@ -140,8 +140,6 @@ is given in the additional document {\tt Library.ps}.
 \end{description}
 
 
-% $Id: RefMan-int.tex 11307 2008-08-06 08:38:57Z jnarboux $ 
-
 %%% Local Variables: 
 %%% mode: latex
 %%% TeX-master: "Reference-Manual"
diff --git a/doc/refman/RefMan-lib.tex b/doc/refman/RefMan-lib.tex
index 2c8abc88..31c6fef4 100644
--- a/doc/refman/RefMan-lib.tex
+++ b/doc/refman/RefMan-lib.tex
@@ -809,7 +809,8 @@ subdirectories:
 \begin{tabular}{lp{12cm}}
   {\bf Logic}   & Classical logic and dependent equality \\
   {\bf Arith}   & Basic Peano arithmetic \\
-  {\bf NArith}  & Basic positive integer arithmetic \\
+  {\bf PArith}  & Basic positive integer arithmetic \\
+  {\bf NArith}  & Basic binary natural number arithmetic \\
   {\bf ZArith}  & Basic relative integer arithmetic \\
   {\bf Numbers} & Various approaches to natural, integer and cyclic numbers (currently axiomatically and on top of 2$^{31}$ binary words) \\
   {\bf Bool}    & Booleans (basic functions and results) \\
@@ -996,7 +997,7 @@ Abort.
 \end{coq_eval}
 
 \item {\tt split\_Rabs} allows to unfold {\tt Rabs} constant and splits 
-corresponding conjonctions.
+corresponding conjunctions.
 \tacindex{split\_Rabs}
 
 \begin{coq_example*}
@@ -1094,8 +1095,6 @@ description, etc.) and the possibility to download them one by one.
 You will also find informations on how to submit a new
 contribution.
 
-% $Id: RefMan-lib.tex 13091 2010-06-08 13:56:19Z herbelin $ 
-
 %%% Local Variables: 
 %%% mode: latex
 %%% TeX-master: "Reference-Manual"
diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex
index d8747254..38ad9aa8 100644
--- a/doc/refman/RefMan-ltac.tex
+++ b/doc/refman/RefMan-ltac.tex
@@ -100,6 +100,7 @@ is understood as
 & | & {\tt progress} {\tacexprpref}\\
 & | & {\tt repeat} {\tacexprpref}\\
 & | & {\tt try} {\tacexprpref}\\
+& | & {\tt timeout} {\it (}{\naturalnumber} {\it |} {\ident}{\it )} {\tacexprpref}\\
 & | & {\tacexprinf} \\
 \\
 {\tacexprinf} & ::= &
@@ -446,6 +447,28 @@ This is a combination of the previous variants.
 
 \ErrMsg \errindex{Tactic Failure {\it message} (level $n$)}.
 
+\subsubsection[Timeout]{Timeout\tacindex{timeout}
+\index{Tacticals!timeout@{\tt timeout}}}
+
+We can force a tactic to stop if it has not finished after a certain
+amount of time:
+\begin{quote}
+{\tt timeout} {\num} {\tacexpr}
+\end{quote}
+{\tacexpr} is evaluated to $v$. $v$ must be a tactic value. $v$ is
+normally applied, except that it is interrupted after ${\num}$ seconds
+if it is still running. In this case the outcome is a failure.
+
+Warning: For the moment, {\tt timeout} is based on elapsed time in
+seconds, which is very
+machine-dependent: a script that works on a quick machine may fail
+on a slow one. The converse is even possible if you combine a
+{\tt timeout} with some other tacticals. This tactical is hence
+proposed only for convenience during debug or other development
+phases, we strongly advise you to not leave any {\tt timeout} in
+final scripts. Note also that this tactical isn't available on
+the native Windows port of Coq.
+
 \subsubsection[Local definitions]{Local definitions\index{Ltac!let}
 \index{Ltac!let rec}
 \index{let!in Ltac}
@@ -568,11 +591,10 @@ pattern:
 \begin{quote}
 {\tt context} {\ident} {\tt [} {\cpattern} {\tt ]}
 \end{quote}
-It matches any term which one subterm matches {\cpattern}. If there is
-a match, the optional {\ident} is assign the ``matched context'', that
-is the initial term where the matched subterm is replaced by a
-hole. The definition of {\tt context} in expressions below will show
-how to use such term contexts.
+It matches any term with a subterm matching {\cpattern}. If there is
+a match, the optional {\ident} is assigned the ``matched context'', i.e.
+the initial term where the matched subterm is replaced by a
+hole. The example below will show how to use such term contexts.
 
 If the evaluation of the right-hand-side of a valid match fails, the
 next matching subterm is tried. If no further subterm matches, the
@@ -606,7 +628,7 @@ Alternatively, one may now use the following variant of {\tt context}:
 The behavior of {\tt appcontext} is the same as the one of {\tt
   context}, except that a matching subterm could be a partial
 part of a longer application. For instance, in {\tt (f 1 2)},
-an {\tt appcontext [f ?x]} will find the matching subterm {\tt (f 1)}.
+an {\tt appcontext [f ?x]} will find the matching subterm {\tt (f 1)}. 
 
 \end{Variants}
 
diff --git a/doc/refman/RefMan-modr.tex b/doc/refman/RefMan-modr.tex
index b2ea232c..9ab8aded 100644
--- a/doc/refman/RefMan-modr.tex
+++ b/doc/refman/RefMan-modr.tex
@@ -556,8 +556,6 @@ In the rules below we assume $\Gamma_P$ is $[p_1:P_1;\ldots;p_r:P_r]$,
 % \end{itemize}
 
 
-% $Id: RefMan-modr.tex 11197 2008-07-01 13:05:41Z soubiran $
-
 %%% Local Variables: 
 %%% mode: latex
 %%% TeX-master: "Reference-Manual"
diff --git a/doc/refman/RefMan-oth.tex b/doc/refman/RefMan-oth.tex
index 025788f5..5b1ad198 100644
--- a/doc/refman/RefMan-oth.tex
+++ b/doc/refman/RefMan-oth.tex
@@ -225,8 +225,7 @@ a subterm that matches the pattern {\termpattern} (holes of the
 pattern are either denoted by ``{\texttt \_}'' or
 by ``{\texttt ?{\ident}}'' when non linear patterns are expected).
 
-\item {\tt SearchAbout [ \nelist{\zeroone{-}{\termpatternorstr}}{}
-].}\\
+\item {\tt SearchAbout \nelist{\zeroone{-}{\termpatternorstr}}{}.}\\
 
 \noindent where {\termpatternorstr} is a
 {\termpattern} or a {\str}, or a {\str} followed by a scope
@@ -241,25 +240,24 @@ search excludes the objects that mention that {\termpattern} or that
 {\str}.
 
 \item
-\begin{tabular}[t]{@{}l}
-  {\tt SearchAbout {\termpatternorstr} inside {\module$_1$} \ldots{} {\module$_n$}.} \\
-  {\tt SearchAbout [ \nelist{{\termpatternorstr}}{} ]
+  {\tt SearchAbout \nelist{{\termpatternorstr}}{}
     inside {\module$_1$} \ldots{} {\module$_n$}.}
-\end{tabular}
 
 This restricts the search to constructions defined in modules
 {\module$_1$} \ldots{} {\module$_n$}.
 
 \item
-\begin{tabular}[t]{@{}l}
-  {\tt SearchAbout {\termpatternorstr} outside {\module$_1$}...{\module$_n$}.} \\
-  {\tt SearchAbout [ \nelist{{\termpatternorstr}}{} ]
+  {\tt SearchAbout \nelist{{\termpatternorstr}}{}
      outside {\module$_1$}...{\module$_n$}.}
-\end{tabular}
 
 This restricts the search to constructions not defined in modules
 {\module$_1$} \ldots{} {\module$_n$}.
 
+\item {\tt SearchAbout [ ... ]. }
+
+For compatibility with older versions, the list of objects to search
+may be enclosed by optional {\tt [  ]} delimiters.
+
 \end{Variants}
 
 \examples
@@ -268,8 +266,8 @@ This restricts the search to constructions not defined in modules
 Require Import ZArith.
 \end{coq_example*}
 \begin{coq_example}
-SearchAbout [ Zmult Zplus "distr" ].
-SearchAbout [ "+"%Z "*"%Z "distr" -positive -Prop].
+SearchAbout Zmult Zplus "distr".
+SearchAbout "+"%Z "*"%Z "distr" -positive -Prop.
 SearchAbout (?x * _ + ?x * _)%Z outside OmegaLemmas.
 \end{coq_example}
 
@@ -338,16 +336,6 @@ This restricts the search to constructions not defined in modules
 
 \end{Variants}
 
-% \subsection[\tt SearchIsos {\term}.]{\tt SearchIsos {\term}.\comindex{SearchIsos}}
-% \label{searchisos}
-% \texttt{SearchIsos} searches terms by their type modulo isomorphism.
-% This command displays the full name of all constants, variables,
-% inductive types, and inductive constructors of the current
-% context whose type is isomorphic to {\term} modulo the contextual part of the
-% following axiomatization (the mutual inductive types with one constructor,
-% without implicit arguments, and for which projections exist, are regarded as a
-% sequence of $\sa{}$):
-
 
 % \begin{tabbing}
 % \ \ \ \ \=11.\ \=\kill
@@ -632,6 +620,12 @@ files is only possible under the bytecode version of {\tt coqtop}
 \ref{Addoc-coqc}), or when Coq has been compiled with a version of
 Objective Caml that supports native {\tt Dynlink} ($\ge$ 3.11).
 
+\begin{Variants}
+\item {\tt Local Declare ML Module {\str$_1$} .. {\str$_n$}.}\\
+  This variant is not exported to the modules that import the module
+  where they occur, even if outside a section.
+\end{Variants}
+
 \begin{ErrMsgs}
 \item \errindex{File not found on loadpath : \str}
 \item \errindex{Loading of ML object file forbidden in a native Coq}
@@ -938,7 +932,7 @@ a {\tt Timeout} are unaffected.
 
 \subsection[\tt Unset Default Timeout.]{\tt Unset Default Timeout.\comindex{Unset Default Timeout}}
 
-This command turns off the use of a defaut timeout.
+This command turns off the use of a default timeout.
 
 \subsection[\tt Test Default Timeout.]{\tt Test Default Timeout.\comindex{Test Default Timeout}}
 
@@ -978,12 +972,6 @@ time of writing this documentation, the default value is 50).
 \subsection[\tt Test Printing Depth.]{\tt Test Printing Depth.\comindex{Test Printing Depth}}
 This command displays the current nesting depth used for display.
 
-%\subsection{\tt Explain ...}
-%Not yet documented.
-
-%\subsection{\tt Go ...}
-%Not yet documented.
-
 %\subsection{\tt Abstraction ...}
 %Not yet documented.
 
@@ -997,7 +985,7 @@ compares applicative terms while the other is a brute-force but efficient
 algorithm that first normalizes the terms before comparing them.  The
 second algorithm is based on a bytecode representation of terms
 similar to the bytecode representation used in the ZINC virtual
-machine~\cite{Leroy90}. It is specially useful for intensive
+machine~\cite{Leroy90}. It is especially useful for intensive
 computation of algebraic values, such as numbers, and for reflexion-based
 tactics. The commands to fine-tune the reduction strategies and the
 lazy conversion algorithm are described first.
@@ -1188,8 +1176,6 @@ control the scope of their effect. There are four kinds of commands:
 \end{itemize}
 
 
-% $Id: RefMan-oth.tex 13923 2011-03-21 16:25:20Z letouzey $ 
-
 %%% Local Variables: 
 %%% mode: latex
 %%% TeX-master: "Reference-Manual"
diff --git a/doc/refman/RefMan-pre.tex b/doc/refman/RefMan-pre.tex
index a2cdb5ec..29de89d8 100644
--- a/doc/refman/RefMan-pre.tex
+++ b/doc/refman/RefMan-pre.tex
@@ -673,7 +673,7 @@ Yves Bertot, Jean-Christophe Filliâtre, Pierre Courtieu and
 Julien Forest acted as maintainers of features they implemented in
 previous versions of Coq.
 
-Julien Narboux contributed to CoqIDE.
+Julien Narboux contributed to {\CoqIDE}.
 Nicolas Tabareau made the adaptation of the interface of the old
 ``setoid rewrite'' tactic to the new version. Lionel Mamane worked on
 the interaction between Coq and its external interfaces. With Samuel
@@ -750,7 +750,7 @@ standard and more robust basis.
 Though invisible from outside, Arnaud Spiwack improved the general
 process of management of existential variables. Pierre Letouzey and
 Stéphane Glondu improved the compilation scheme of the Coq archive.
-Vincent Gross provided support to CoqIDE. Jean-Marc Notin provided
+Vincent Gross provided support to {\CoqIDE}. Jean-Marc Notin provided
 support for benchmarking and archiving.
 
 Many users helped by reporting problems, providing patches, suggesting
@@ -768,6 +768,150 @@ Paris, April 2010\\
 Hugo Herbelin\\
 \end{flushright}
 
+\section*{Credits: version 8.4}
+
+{\Coq} version 8.4 contains the result of three long-term projects: a
+new modular library of arithmetic by Pierre Letouzey, a new proof
+engine by Arnaud Spiwack and a new communication protocol for {\CoqIDE}
+by Vincent Gross.
+
+The new modular library of arithmetic extends, generalizes and
+unifies the existing libraries on Peano arithmetic (types {\tt nat},
+{\tt N} and {\tt BigN}), positive arithmetic (type {\tt positive}),
+integer arithmetic ({\tt Z} and {\tt BigZ}) and machine word
+arithmetic (type {\tt Int31}). It provides with unified notations
+(e.g. systematic use of {\tt add} and {\tt mul} for denoting the
+addition and multiplication operators), systematic and generic
+development of operators and properties of these operators for all the
+types mentioned above, including gcd, pcm, power, square root, base 2
+logarithm, division, modulo, bitwise operations, logical shifts,
+comparisons, iterators, ...
+
+The most visible feature of the new proof engine is the support for
+structured scripts (bullets and proof brackets) but, even if yet not
+user-available, the new engine also provides the basis for refining
+existential variables using tactics, for applying tactics to several
+goals simultaneously, for reordering goals, all features which are
+planned for the next release.
+
+Before version 8.4, {\CoqIDE} was linked to {\Coq} with the graphical
+interface living in a separate thread. From version 8.4, {\CoqIDE} is a
+separate process communicating with {\Coq} through a textual
+channel. This allows for a more robust interfacing, the ability to
+interrupt {\Coq} without interrupting the interface, and the ability to
+manage several sessions in parallel. Relying on the infrastructure
+work made by Vincent Gross, Pierre Letouzey, Pierre Boutillier and
+Pierre-Marie P\'edrot contributed many various refinements of {\CoqIDE}.
+
+{\Coq} 8.4 also comes with a bunch of many various smaller-scale changes
+and improvements regarding the different components of the system.
+
+The underlying logic has been extended with $\eta$-conversion thanks
+to Hugo Herbelin, St\'ephane Glondu and Benjamin Gr\'egoire. The
+addition of $\eta$-conversion is justified by the confidence that the
+formulation of the Calculus of Inductive Constructions based on typed
+equality (such as the one considered in Lee and Werner to build a
+set-theoretic model of CIC~\cite{LeeWerner11}) is applicable to the
+concrete implementation of {\Coq}.
+
+The underlying logic benefited also from a refinement of the guard
+condition for fixpoints by Pierre Boutillier, the point being that it
+is safe to propagate the information about structurally smaller
+arguments through $\beta$-redexes that are blocked by the
+``match'' construction (blocked commutative cuts).
+
+Relying on the added permissiveness of the guard condition, Hugo
+Herbelin could extend the pattern-matching compilation algorithm
+so that matching over a sequence of terms involving
+dependencies of a term or of the indices of the type of a term in the
+type of other terms is systematically supported.
+
+Regarding the high-level specification language, Pierre Boutillier
+introduced the ability to give implicit arguments to anonymous
+functions, Hugo Herbelin introduced the ability to define notations
+with several binders (e.g. \verb=exists x y z, P=), Matthieu Sozeau
+made the type classes inference mechanism more robust and predictable,
+Enrico Tassi introduced a command {\tt Arguments} that generalizes
+{\tt Implicit Arguments} and {\tt Arguments Scope} for assigning
+various properties to arguments of constants. Various improvements in
+the type inference algorithm were provided by Matthieu Sozeau and Hugo
+Herbelin with contributions from Enrico Tassi.
+
+Regarding tactics, Hugo Herbelin introduced support for referring to
+expressions occurring in the goal by pattern in tactics such as {\tt
+  set} or {\tt destruct}. Hugo Herbelin also relied on ideas from
+Chung-Kil Hur's {\tt Heq} plugin to introduce automatic computation of
+occurrences to generalize when using {\tt destruct} and {\tt
+  induction} on types with indices.  St\'ephane Glondu introduced new
+tactics {\tt constr\_eq}, {\tt is\_evar} and {\tt has\_evar} to be
+used when writing complex tactics.  Enrico Tassi added support to
+fine-tuning the behavior of {\tt simpl}. Enrico Tassi added the
+ability to specify over which variables of a section a lemma has
+to be exactly generalized.  Pierre Letouzey added a tactic {\tt
+  timeout} and the interruptibility of {\tt vm\_compute}.  Bug fixes
+and miscellaneous improvements of the tactic language came from Hugo
+Herbelin, Pierre Letouzey and Matthieu Sozeau.
+
+Regarding decision tactics, Lo\"ic Pottier maintained {\tt Nsatz},
+moving in particular to a type-class based reification of goals while
+Fr\'ed\'eric Besson maintained {\tt Micromega}, adding in particular
+support for division.
+
+Regarding vernacular commands, St\'ephane Glondu provided new commands
+to analyze the structure of type universes.
+
+Regarding libraries, a new library about lists of a given length
+(called vectors) has been provided by Pierre Boutillier.
+
+Pierre Corbineau maintained the C-zar proof mode.
+
+Bruno Barras and Benjamin Gr\'egoire maintained the call-by-value
+reduction machines.
+
+The extraction mechanism benefited from several improvements provided by
+Pierre Letouzey.
+
+Pierre Letouzey maintained the module system, with contributions from
+\'Elie Soubiran.
+
+Julien Forest maintained the {\tt Function} command.
+
+Matthieu Sozeau maintained the setoid rewriting mechanism.
+
+{\Coq} related tools have been upgraded too. In particular, {\tt
+  coq\_makefile} has been largely revised by Pierre Boutillier.
+
+Bruno Barras and Pierre Letouzey maintained the {\tt coqchk} checker.
+
+Pierre Courtieu and Arnaud Spiwack contributed new features for using
+{\Coq} through Proof General.
+
+Under the hood, the {\Coq} architecture benefited from improvements in
+terms of efficiency and robustness thanks to Pierre Letouzey and Yann
+R\'egis-Gianas with contributions from St\'ephane Glondu and Matthias
+Puech. The build system is maintained by Pierre Letouzey with
+contributions from St\'ephane Glondu and Pierre Boutillier.
+
+The general maintenance was done by Hugo Herbelin, Pierre Letouzey,
+Pierre Boutillier and St\'ephane Glondu with local contributions from
+Guillaume Melquiond and Julien Narboux.
+
+Packaging tools were provided by Pierre Letouzey (Windows), Pierre
+Boutillier (MacOS), St\'ephane Glondu (Debian). Releasing, testing and
+benchmarking support was provided by Jean-Marc Notin.
+
+Many suggestions for improvements were motivated by feedback from
+users, on either the bug tracker or the coq-club mailing list. Special
+thanks are going to the users who contributed patches, starting with
+Tom Prince. Other patch contributors include C\'edric Auger, David
+Baelde, Dan Grayson, Paolo Herms, Robbert Krebbers, Marc Lasson,
+Hendrik Tews and Eelis van der Weegen.
+
+\begin{flushright}
+Paris, December 2011\\
+Hugo Herbelin\\
+\end{flushright}
+
 %new Makefile
 
 %\newpage
@@ -775,7 +919,7 @@ Hugo Herbelin\\
 % Integration of ZArith lemmas from Sophia and Nijmegen.
 
 
-% $Id: RefMan-pre.tex 13271 2010-07-08 18:10:54Z herbelin $ 
+% $Id: RefMan-pre.tex 14853 2011-12-23 19:59:48Z herbelin $ 
 
 %%% Local Variables: 
 %%% mode: latex
diff --git a/doc/refman/RefMan-pro.tex b/doc/refman/RefMan-pro.tex
index 3a8936eb..e5dc669d 100644
--- a/doc/refman/RefMan-pro.tex
+++ b/doc/refman/RefMan-pro.tex
@@ -133,6 +133,24 @@ one gulp, as a proof term (see Section~\ref{exact}).
 
 \SeeAlso {\tt Proof with {\tac}.} in Section~\ref{ProofWith}.
 
+\subsection[\tt Proof using {\ident$_1$ \dots {\ident$_n$}}.]
+{\tt Proof using {\ident$_1$ \dots {\ident$_n$}}.
+\comindex{Proof using} \label{ProofUsing}}
+
+This command applies in proof editing mode. 
+It declares the set of section variables (see~\ref{Variable}) 
+used by the proof. At {\tt Qed} time, the system will assert that 
+the set of section variables actually used in the proof is a subset of
+the declared one.
+
+The set of declared variables is closed under type dependency.
+For example if {\tt T} is variable and {\tt a} is a variable of
+type {\tt T}, the commands {\tt Proof using a} and
+{\tt Proof using T a} are actually equivalent.
+
+\variant {\tt Proof using {\ident$_1$ \dots {\ident$_n$}} with {\tac}.} 
+in Section~\ref{ProofWith}.
+
 \subsection[\tt Abort.]{\tt Abort.\comindex{Abort}}
 
 This command cancels the current proof development, switching back to
@@ -211,7 +229,6 @@ backtracks one step.
 
 \begin{ErrMsgs}
 \item \errindex{No focused proof (No proof-editing in progress)}
-\item \errindex{Undo stack would be exhausted}
 \end{ErrMsgs}
 
 \begin{Variants}
@@ -222,18 +239,6 @@ backtracks one step.
 
 \end{Variants}
 
-\subsection[\tt Set Undo {\num}.]{\tt Set Undo {\num}.\comindex{Set Undo}}
-
-This command changes the maximum number of {\tt Undo}'s that will be
-possible when doing a proof. It only affects proofs started after
-this command, such that if you want to change the current undo limit
-inside a proof, you should first restart this proof.
-
-\subsection[\tt Unset Undo.]{\tt Unset Undo.\comindex{Unset Undo}}
-
-This command resets the default number of possible {\tt Undo} commands
-(which is currently 12).
-
 \subsection[\tt Restart.]{\tt Restart.\comindex{Restart}}
 This command restores the proof editing process to the original goal.
 
@@ -362,8 +367,6 @@ All the hypotheses remains usable in the proof development.
 This command goes back to the default mode which is to print all
 available hypotheses.
 
-% $Id: RefMan-pro.tex 13091 2010-06-08 13:56:19Z herbelin $
-
 
 \subsection[\tt Set Automatic Introduction.]{\tt Set Automatic Introduction.\comindex{Set Automatic Introduction}\comindex{Unset Automatic Introduction}\label{Set Automatic Introduction}}
 
diff --git a/doc/refman/RefMan-syn.tex b/doc/refman/RefMan-syn.tex
index 2b0d636e..ea3d55f2 100644
--- a/doc/refman/RefMan-syn.tex
+++ b/doc/refman/RefMan-syn.tex
@@ -345,7 +345,7 @@ Infix "/\" := and (at level 80, right associativity).
 
 \subsection{Reserving notations
 \label{ReservedNotation}
-\comindex{ReservedNotation}}
+\comindex{Reserved Notation}}
 
 A given notation may be used in different contexts. {\Coq} expects all
 uses of the notation to be defined at the same precedence and with the
@@ -774,32 +774,57 @@ To bind a delimiting key to a scope, use the command
 \end{quote}
 
 \subsubsection{Binding arguments of a constant to an interpretation scope
-\comindex{Arguments Scope}}
+\comindex{Arguments}}
 
 It is possible to set in advance that some arguments of a given
 constant have to be interpreted in a given scope. The command is
 \begin{quote}
-{\tt Arguments Scope} {\qualid} {\tt [ \nelist{\optscope}{} ]}
+{\tt Arguments} {\qualid} \nelist{\name {\tt \%}\scope}{}
 \end{quote}
-where the list is a list made either of {\tt \_} or of a scope name.
-Each scope in the list is bound to the corresponding parameter of
-{\qualid} in order.  When interpreting a term, if some of the
+where the list is the list of the arguments of {\qualid} eventually
+annotated with their {\scope}. Grouping round parentheses can
+be used to decorate multiple arguments with the same scope.
+{\scope} can be either a scope name or its delimiting key. For example
+the following command puts the first two arguments of {\tt plus\_fct}
+in the scope delimited by the key {\tt F} ({\tt Rfun\_scope}) and the
+last argument in the scope delimited by the key {\tt R} ({\tt R\_scope}).
+
+\begin{coq_example*}
+Arguments plus_fct (f1 f2)%F x%R.
+\end{coq_example*}
+
+The {\tt Arguments} command accepts scopes decoration to all grouping
+parentheses. In the following example arguments {\tt A} and {\tt B} 
+are marked as maximally inserted implicit arguments and are
+put into the {\tt type\_scope} scope.
+
+\begin{coq_example*}
+Arguments respectful {A B}%type (R R')%signature _ _.
+\end{coq_example*}
+
+When interpreting a term, if some of the
 arguments of {\qualid} are built from a notation, then this notation
 is interpreted in the scope stack extended by the scopes bound (if any)
 to these arguments.
 
+Arguments scopes can be cleared with the following command:
+
+\begin{quote}
+{\tt Arguments {\qualid} : clear scopes}
+\end{quote}
+
 \begin{Variants}
-\item {\tt Global Arguments Scope} {\qualid} {\tt [ \nelist{\optscope}{} ]}
+\item {\tt Global Arguments} {\qualid} \nelist{\name {\tt \%}\scope}{}
 
-This behaves like {\tt Arguments Scope} {\qualid} {\tt [
-\nelist{\optscope}{} ]} but survives when a section is closed instead
+This behaves like {\tt Arguments} {\qualid} \nelist{\name {\tt \%}\scope}{}
+but survives when a section is closed instead
 of stopping working at section closing. Without the {\tt Global} modifier,
 the effect of the command stops when the section it belongs to ends.
 
-\item {\tt Local Arguments Scope} {\qualid} {\tt [ \nelist{\optscope}{} ]}
+\item {\tt Local Arguments} {\qualid} \nelist{\name {\tt \%}\scope}{}
 
-This behaves like {\tt Arguments Scope} {\qualid} {\tt [
-    \nelist{\optscope}{} ]} but does not survive modules and files.
+This behaves like {\tt Arguments} {\qualid} \nelist{\name {\tt \%}\scope}{}
+but does not survive modules and files.
 Without the {\tt Local} modifier, the effect of the command is
 visible from within other modules or files.
 
@@ -861,7 +886,7 @@ declared or defined constant.
 
 We give an overview of the scopes used in the standard library of
 {\Coq}. For a complete list of notations in each scope, use the
-commands {\tt Print Scopes} or {\tt Print Scopes {\scope}}.
+commands {\tt Print Scopes} or {\tt Print Scope {\scope}}.
 
 \subsubsection{\tt type\_scope}
 
@@ -1047,7 +1072,8 @@ at the time of use of the abbreviation.
 %except that abbreviations are used for printing (unless the modifier
 %\verb=(only parsing)= is given) while syntactic definitions were not.
 
-\section{Tactic Notations}
+\section{Tactic Notations
+\comindex{Tactic Notation}}
 
 Tactic notations allow to customize the syntax of the tactics of the
 tactic language\footnote{Tactic notations are just a simplification of
@@ -1140,8 +1166,6 @@ places where a list of the underlying entry can be used: {\nterm{entry}} is
 either {\tt\small constr}, {\tt\small hyp}, {\tt\small integer} or
 {\tt\small int\_or\_var}.
 
-% $Id: RefMan-syn.tex 13329 2010-07-26 11:05:39Z herbelin $ 
-
 %%% Local Variables: 
 %%% mode: latex
 %%% TeX-master: "Reference-Manual"
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index 14d95ab8..198f8f30 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -497,6 +497,89 @@ Section~\ref{pattern} to transform the goal so that it gets the form
 
 \end{Variants}
 
+\subsection{{\tt apply {\term} in {\ident}}
+\tacindex{apply \ldots\ in}}
+
+This tactic applies to any goal.  The argument {\term} is a term
+well-formed in the local context and the argument {\ident} is an
+hypothesis of the context.  The tactic {\tt apply {\term} in {\ident}}
+tries to match the conclusion of the type of {\ident} against a non
+dependent premise of the type of {\term}, trying them from right to
+left.  If it succeeds, the statement of hypothesis {\ident} is
+replaced by the conclusion of the type of {\term}. The tactic also
+returns as many subgoals as the number of other non dependent premises
+in the type of {\term} and of the non dependent premises of the type
+of {\ident}.  If the conclusion of the type of {\term} does not match
+the goal {\em and} the conclusion is an inductive type isomorphic to a
+tuple type, then the tuple is (recursively) decomposed and the first
+component of the tuple of which a non dependent premise matches the
+conclusion of the type of {\ident}. Tuples are decomposed in a
+width-first left-to-right order (for instance if the type of {\tt H1}
+is a \verb=A <-> B= statement, and the type of {\tt H2} is \verb=A=
+then {\tt apply H1 in H2} transforms the type of {\tt H2} into {\tt
+  B}). The tactic {\tt apply} relies on first-order pattern-matching
+with dependent types.
+
+\begin{ErrMsgs}
+\item \errindex{Statement without assumptions}
+
+This happens if the type of {\term} has no non dependent premise.
+
+\item \errindex{Unable to apply}
+
+This happens if the conclusion of {\ident} does not match any of the
+non dependent premises of the type of {\term}.
+\end{ErrMsgs}
+
+\begin{Variants}
+\item {\tt apply \nelist{\term}{,} in {\ident}}
+
+This applies each of {\term} in sequence in {\ident}.
+
+\item {\tt apply \nelist{{\term} with {\bindinglist}}{,} in {\ident}}
+
+This does the same but uses the bindings in each {\bindinglist} to 
+instantiate the parameters of the corresponding type of {\term}
+(see syntax of bindings in Section~\ref{Binding-list}).
+
+\item {\tt eapply \nelist{{\term} with {\bindinglist}}{,} in {\ident}}
+\tacindex{eapply {\ldots} in}
+
+This works as {\tt apply \nelist{{\term} with {\bindinglist}}{,} in
+{\ident}} but turns unresolved bindings into existential variables, if
+any, instead of failing.
+
+\item {\tt apply \nelist{{\term}{,} with {\bindinglist}}{,} in {\ident} as {\disjconjintropattern}}
+
+This works as {\tt apply \nelist{{\term}{,} with {\bindinglist}}{,} in
+{\ident}} then destructs the hypothesis {\ident} along
+{\disjconjintropattern} as {\tt destruct {\ident} as
+{\disjconjintropattern}} would.
+
+\item {\tt eapply \nelist{{\term}{,} with {\bindinglist}}{,} in {\ident} as {\disjconjintropattern}}
+
+This works as {\tt apply \nelist{{\term}{,} with {\bindinglist}}{,} in {\ident} as {\disjconjintropattern}} but using {\tt eapply}.
+
+\item {\tt simple apply {\term} in {\ident}}
+\tacindex{simple apply {\ldots} in} 
+\tacindex{simple eapply {\ldots} in} 
+
+This behaves like {\tt apply {\term} in {\ident}} but it reasons
+modulo conversion only on subterms that contain no variables to
+instantiate. For instance, if {\tt id := fun x:nat => x} and {\tt H :
+  forall y, id y = y -> True} and {\tt H0 : O = O} then {\tt simple
+  apply H in H0} does not succeed because it would require the
+conversion of {\tt f ?y} and {\tt O} where {\tt ?y} is a variable to
+instantiate.  Tactic {\tt simple apply {\term} in {\ident}} does not
+either traverse tuples as {\tt apply {\term} in {\ident}} does.
+
+\item {\tt \zeroone{simple} apply \nelist{{\term} \zeroone{with {\bindinglist}}}{,} in {\ident} \zeroone{as {\disjconjintropattern}}}\\
+{\tt \zeroone{simple} eapply \nelist{{\term} \zeroone{with {\bindinglist}}}{,} in {\ident} \zeroone{as {\disjconjintropattern}}}
+
+This summarizes the different syntactic variants of {\tt apply {\term}
+  in {\ident}} and {\tt eapply {\term} in {\ident}}.
+\end{Variants}
+
 \subsection{{\tt set ( {\ident} {\tt :=} {\term} \tt )}
 \label{tactic:set}
 \tacindex{set}
@@ -508,6 +591,11 @@ hypotheses of the current goal and adds the new definition {\ident
 {\tt :=} \term} to the local context. The default is to make this
 replacement only in the conclusion.
 
+If {\term} has holes (i.e. subexpressions of the form ``\_''), the
+tactic first checks that all subterms matching the pattern are
+compatible before doing the replacement using the leftmost subterm
+matching the pattern.
+
 \begin{Variants}
 
 \item {\tt set (} {\ident} {\tt :=} {\term} {\tt ) in {\occgoalset}}
@@ -543,7 +631,7 @@ Section~\ref{Occurrences clauses}.
   This is a more general form of {\tt remember} that remembers the
   occurrences of {\term} specified by an occurrences set.
 
-\item {\tt pose (  {\ident} {\tt :=} {\term} {\tt )}}
+\item {\tt pose ( {\ident} := {\term} )}
   
   This adds the local definition {\ident} := {\term} to the current
   context without performing any replacement in the goal or in the
@@ -660,89 +748,6 @@ in the list of subgoals remaining to prove.
 
 \end{Variants}
 
-\subsection{{\tt apply {\term} in {\ident}}
-\tacindex{apply \ldots\ in}}
-
-This tactic applies to any goal.  The argument {\term} is a term
-well-formed in the local context and the argument {\ident} is an
-hypothesis of the context.  The tactic {\tt apply {\term} in {\ident}}
-tries to match the conclusion of the type of {\ident} against a non
-dependent premise of the type of {\term}, trying them from right to
-left.  If it succeeds, the statement of hypothesis {\ident} is
-replaced by the conclusion of the type of {\term}. The tactic also
-returns as many subgoals as the number of other non dependent premises
-in the type of {\term} and of the non dependent premises of the type
-of {\ident}.  If the conclusion of the type of {\term} does not match
-the goal {\em and} the conclusion is an inductive type isomorphic to a
-tuple type, then the tuple is (recursively) decomposed and the first
-component of the tuple of which a non dependent premise matches the
-conclusion of the type of {\ident}. Tuples are decomposed in a
-width-first left-to-right order (for instance if the type of {\tt H1}
-is a \verb=A <-> B= statement, and the type of {\tt H2} is \verb=A=
-then {\tt apply H1 in H2} transforms the type of {\tt H2} into {\tt
-  B}). The tactic {\tt apply} relies on first-order pattern-matching
-with dependent types.
-
-\begin{ErrMsgs}
-\item \errindex{Statement without assumptions}
-
-This happens if the type of {\term} has no non dependent premise.
-
-\item \errindex{Unable to apply}
-
-This happens if the conclusion of {\ident} does not match any of the
-non dependent premises of the type of {\term}.
-\end{ErrMsgs}
-
-\begin{Variants}
-\item {\tt apply \nelist{\term}{,} in {\ident}}
-
-This applies each of {\term} in sequence in {\ident}.
-
-\item {\tt apply \nelist{{\term} with {\bindinglist}}{,} in {\ident}}
-
-This does the same but uses the bindings in each {\bindinglist} to 
-instantiate the parameters of the corresponding type of {\term}
-(see syntax of bindings in Section~\ref{Binding-list}).
-
-\item {\tt eapply \nelist{{\term} with {\bindinglist}}{,} in {\ident}}
-\tacindex{eapply {\ldots} in}
-
-This works as {\tt apply \nelist{{\term} with {\bindinglist}}{,} in
-{\ident}} but turns unresolved bindings into existential variables, if
-any, instead of failing.
-
-\item {\tt apply \nelist{{\term}{,} with {\bindinglist}}{,} in {\ident} as {\disjconjintropattern}}
-
-This works as {\tt apply \nelist{{\term}{,} with {\bindinglist}}{,} in
-{\ident}} then destructs the hypothesis {\ident} along
-{\disjconjintropattern} as {\tt destruct {\ident} as
-{\disjconjintropattern}} would.
-
-\item {\tt eapply \nelist{{\term}{,} with {\bindinglist}}{,} in {\ident} as {\disjconjintropattern}}
-
-This works as {\tt apply \nelist{{\term}{,} with {\bindinglist}}{,} in {\ident} as {\disjconjintropattern}} but using {\tt eapply}.
-
-\item {\tt simple apply {\term} in {\ident}}
-\tacindex{simple apply {\ldots} in} 
-\tacindex{simple eapply {\ldots} in} 
-
-This behaves like {\tt apply {\term} in {\ident}} but it reasons
-modulo conversion only on subterms that contain no variables to
-instantiate. For instance, if {\tt id := fun x:nat => x} and {\tt H :
-  forall y, id y = y -> True} and {\tt H0 : O = O} then {\tt simple
-  apply H in H0} does not succeed because it would require the
-conversion of {\tt f ?y} and {\tt O} where {\tt ?y} is a variable to
-instantiate.  Tactic {\tt simple apply {\term} in {\ident}} does not
-either traverse tuples as {\tt apply {\term} in {\ident}} does.
-
-\item {\tt \zeroone{simple} apply \nelist{{\term} \zeroone{with {\bindinglist}}}{,} in {\ident} \zeroone{as {\disjconjintropattern}}}\\
-{\tt \zeroone{simple} eapply \nelist{{\term} \zeroone{with {\bindinglist}}}{,} in {\ident} \zeroone{as {\disjconjintropattern}}}
-
-This summarizes the different syntactic variants of {\tt apply {\term}
-  in {\ident}} and {\tt eapply {\term} in {\ident}}.
-\end{Variants}
-
 \subsection{\tt generalize \term
 \tacindex{generalize}
 \label{generalize}}
@@ -950,7 +955,8 @@ existential variable.
 \tacindex{instantiate}
 \label{instantiate}}
 
-The {\tt instantiate} tactic allows to solve an existential variable
+The {\tt instantiate} tactic allows to refine (see Section~\ref{refine})
+an existential variable
 with the term \term. The \num\  argument is the position of the
 existential variable from right to left in the conclusion. This cannot be
 the number of the existential variable since this number is different
@@ -1296,8 +1302,8 @@ computational expressions (i.e. with few dead code).
 \item {\tt lazy [\qualid$_1$\ldots\qualid$_k$]}\\
       {\tt lazy -[\qualid$_1$\ldots\qualid$_k$]}
 
-  These are respectively synonyms of {\tt cbv beta delta
-  [\qualid$_1$\ldots\qualid$_k$] iota zeta} and {\tt cbv beta delta
+  These are respectively synonyms of {\tt lazy beta delta
+  [\qualid$_1$\ldots\qualid$_k$] iota zeta} and {\tt lazy beta delta
   -[\qualid$_1$\ldots\qualid$_k$] iota zeta}.
 
 \item {\tt vm\_compute} \tacindex{vm\_compute}
@@ -1361,6 +1367,55 @@ by {\tt plus' := plus} is possibly unfolded and reused in the
 recursive calls, but a constant such as {\tt succ := plus (S O)} is
 never unfolded.
 
+The behaviour of {\tt simpl} can be tuned using the {\tt Arguments} vernacular
+command as follows:
+\begin{itemize}
+\item
+A constant can be marked to be never unfolded by {\tt simpl}:
+\begin{coq_example*}
+Arguments minus x y : simpl never
+\end{coq_example*}
+After that command an expression like {\tt (minus (S x) y)} is left untouched by
+the {\tt simpl} tactic.
+\item
+A constant can be marked to be unfolded only if applied to enough arguments.
+The number of arguments required can be specified using
+the {\tt /} symbol in the arguments list of the {\tt Arguments} vernacular
+command.
+\begin{coq_example*}
+Definition fcomp A B C f (g : A -> B) (x : A) : C := f (g x).
+Notation "f \o g" := (fcomp f g) (at level 50).
+Arguments fcomp {A B C} f g x /.
+\end{coq_example*}
+After that command the expression {\tt (f \verb+\+o g)} is left untouched by 
+{\tt simpl} while {\tt ((f \verb+\+o g) t)} is reduced to {\tt (f (g t))}.
+The same mechanism can be used to make a constant volatile, i.e. always 
+unfolded by {\tt simpl}.
+\begin{coq_example*}
+Definition volatile := fun x : nat => x.
+Arguments volatile / x.
+\end{coq_example*}
+\item
+A constant can be marked to be unfolded only if an entire set of arguments
+evaluates to a constructor. The {\tt !} symbol can be used to mark such
+arguments.
+\begin{coq_example*}
+Arguments minus !x !y.
+\end{coq_example*}
+After that command, the expression {\tt (minus (S x) y)} is left untouched by
+{\tt simpl}, while {\tt (minus (S x) (S y))} is reduced to {\tt (minus x y)}.
+\item
+A special heuristic to determine if a constant has to be unfolded can be
+activated with the following command:
+\begin{coq_example*}
+Arguments minus x y : simpl nomatch
+\end{coq_example*}
+The heuristic avoids to perform a simplification step that would
+expose a {\tt match} construct in head position. For example the
+expression {\tt (minus (S (S x)) (S y))} is simplified to
+{\tt (minus (S x) y)} even if an extra simplification is possible.
+\end{itemize}
+
 \tacindex{simpl \dots\ in}
 \begin{Variants}
 \item {\tt simpl {\term}}
@@ -1626,18 +1681,16 @@ Section~\ref{Cic-inductive-definitions}).
 \subsection{\tt induction \term
 \tacindex{induction}}
 
-This tactic applies to any goal. The type of the argument {\term} must
-be an inductive constant. Then, the tactic {\tt induction}
-generates subgoals, one for each possible form of {\term}, i.e. one
-for each constructor of the inductive type.
+This tactic applies to any goal. The argument {\term} must be of
+inductive type and the tactic {\tt induction} generates subgoals,
+one for each possible form of {\term}, i.e. one for each constructor
+of the inductive type.
 
-The tactic {\tt induction} automatically replaces every occurrences
-of {\term} in the conclusion and the hypotheses of the goal.  It
-automatically adds induction hypotheses (using names of the form {\tt
-  IHn1}) to the local context. If some hypothesis must not be taken
-into account in the induction hypothesis, then it needs to be removed
-first (you can also use the tactics {\tt elim} or {\tt simple induction},
-see below).
+If the argument is dependent in either the conclusion or some
+hypotheses of the goal, the argument is replaced by the appropriate
+constructor form in each of the resulting subgoals and induction
+hypotheses are added to the local context using names whose prefix is
+{\tt IH}.
 
 There are particular cases:
 
@@ -1649,10 +1702,13 @@ behaves as {\tt intros until {\ident}; induction {\ident}}.
 
 \item If {\term} is a {\num}, then {\tt induction {\num}} behaves as
 {\tt intros until {\num}} followed by {\tt induction} applied to the
-last introduced hypothesis.
+last introduced hypothesis. Remark: For simple induction on a numeral,
+use syntax {\tt induction ({\num})} (not very interesting anyway).
 
-\Rem For simple induction on a numeral, use syntax {\tt induction
-({\num})} (not very interesting anyway).
+\item The argument {\term} can also be a pattern of which holes are
+  denoted by ``\_''. In this case, the tactic checks that all subterms
+  matching the pattern in the conclusion and the hypotheses are
+  compatible and performs induction using this subterm.
 
 \end{itemize}
 
@@ -1840,10 +1896,19 @@ instantiate premises of the type of {\term$_2$}.
 \tacindex{destruct}}
 \label{destruct}
 
-The tactic {\tt destruct} is used to perform case analysis without
-recursion. Its behavior is similar to {\tt induction} except
-that no induction hypothesis is generated.  It applies to any goal and
-the type of {\term} must be inductively defined. There are particular cases:
+This tactic applies to any goal. The argument {\term} must be of
+inductive or coinductive type and the tactic generates subgoals, one
+for each possible form of {\term}, i.e. one for each constructor of
+the inductive or coinductive type. Unlike {\tt induction}, no
+induction hypothesis is generated by {\tt destruct}.
+
+If the argument is dependent in either the conclusion or some
+hypotheses of the goal, the argument is replaced by the appropriate
+constructor form in each of the resulting subgoals, thus performing
+case analysis. If non dependent, the tactic simply exposes the
+inductive or coinductive structure of the argument.
+
+There are special cases:
 
 \begin{itemize}
 
@@ -1853,10 +1918,13 @@ behaves as {\tt intros until {\ident}; destruct {\ident}}.
 
 \item If {\term} is a {\num}, then {\tt destruct {\num}} behaves as
 {\tt intros until {\num}} followed by {\tt destruct} applied to the
-last introduced hypothesis.
+last introduced hypothesis. Remark: For destruction of a numeral, use
+syntax {\tt destruct ({\num})} (not very interesting anyway).
 
-\Rem For destruction of a numeral, use syntax {\tt destruct
-({\num})} (not very interesting anyway).
+\item The argument {\term} can also be a pattern of which holes are
+  denoted by ``\_''. In this case, the tactic checks that all subterms
+  matching the pattern in the conclusion and the hypotheses are
+  compatible and performs case analysis using this subterm.
 
 \end{itemize}
 
@@ -2599,12 +2667,7 @@ This tactic solves a goal of the form
 {\tt forall $x$ $y$:$R$, \{$x$=$y$\}+\{\verb|~|$x$=$y$\}}, where $R$
 is an inductive type such that its constructors do not take proofs or
 functions as arguments, nor objects in dependent types.
-
-\begin{Variants}
-\item {\tt decide equality {\term}$_1$ {\term}$_2$ }.\\
- Solves a goal of the form {\tt \{}\term$_1${\tt =}\term$_2${\tt
-\}+\{\verb|~|}\term$_1${\tt =}\term$_2${\tt \}}.
-\end{Variants}
+It solves goals of the form {\tt \{$x$=$y$\}+\{\verb|~|$x$=$y$\}} as well.
 
 \subsection{\tt compare \term$_1$ \term$_2$
 \tacindex{compare}}
@@ -2696,7 +2759,7 @@ If {\term} is a proof of a statement of conclusion
 then {\tt injection} applies injectivity as deep as possible to
 derive the equality of all the subterms of {\term$_1$} and {\term$_2$}
 placed in the same positions. For example, from {\tt (S
-  (S n))=(S (S (S m))} we may derive {\tt n=(S m)}.  To use this
+  (S n))=(S (S (S m)))} we may derive {\tt n=(S m)}.  To use this
 tactic {\term$_1$} and {\term$_2$} should be elements of an inductive
 set and they should be neither explicitly equal, nor structurally
 different. We mean by this that, if {\tt n$_1$} and {\tt n$_2$} are
@@ -4042,7 +4105,9 @@ databases are non empty and can be used.
 \begin{description}
 
 \item[\tt core] This special database is automatically used by
-  \texttt{auto}. It contains only basic lemmas about negation,
+  \texttt{auto}, except when pseudo-database \texttt{nocore} is
+  given to \texttt{auto}. The \texttt{core} database contains
+  only basic lemmas about negation,
   conjunction, and so on from. Most of the hints in this database come 
   from the \texttt{Init} and \texttt{Logic} directories.
 
@@ -4174,6 +4239,16 @@ e.g. \texttt{Require Import A.}).
 
 \SeeAlso {\tt Proof.} in Section~\ref{BeginProof}.
 
+\begin{Variants}
+\item {\tt Proof with {\tac} using {\ident$_1$ \dots {\ident$_n$}}}
+  Combines in a single line {\tt Proof with} and {\tt Proof using}, 
+  see~\ref{ProofUsing}
+\item {\tt Proof using {\ident$_1$ \dots {\ident$_n$}} with {\tac}}
+  Combines in a single line {\tt Proof with} and {\tt Proof using}, 
+  see~\ref{ProofUsing}
+
+\end{Variants}
+
 \subsubsection[\tt Declare Implicit Tactic {\tac}.]{\tt Declare Implicit Tactic {\tac}.\comindex{Declare Implicit Tactic}}
 
 This command declares a tactic to be used to solve implicit arguments
@@ -4230,7 +4305,8 @@ general principle of mutual induction for objects in type {\term$_i$}.
 \item {\tt Scheme Equality for \ident$_1$\comindex{Scheme Equality}}
 
   Tries to generate a boolean equality and a proof of the
-  decidability of the usual equality.
+  decidability of the usual equality. If \ident$_i$ involves
+  some other inductive types, their equality has to be defined first.
 
 \item {\tt Scheme Induction for \ident$_1$ Sort {\sort$_1$} \\
   with\\
@@ -4332,8 +4408,6 @@ Chapter~\ref{TacticLanguage} gives examples of more complex
 user-defined tactics.
 
 
-% $Id: RefMan-tac.tex 14762 2011-12-04 20:48:36Z herbelin $ 
-
 %%% Local Variables: 
 %%% mode: latex
 %%% TeX-master: "Reference-Manual"
diff --git a/doc/refman/RefMan-uti.tex b/doc/refman/RefMan-uti.tex
index 5f201b67..bda4cff9 100644
--- a/doc/refman/RefMan-uti.tex
+++ b/doc/refman/RefMan-uti.tex
@@ -84,85 +84,42 @@ modules.
 
 The writing of a generic and complete {\tt Makefile} may be a tedious work
 and that's why \Coq\ provides a tool to automate its creation,
-{\tt coq\_makefile}. Given the files to compile, the command {\tt
-coq\_makefile} prints a 
-{\tt Makefile} on the standard output. So one has just to run the
-command:
+{\tt coq\_makefile}.
 
-\begin{quotation}
-\texttt{\% coq\_makefile} {\em file$_1$.v \dots\ file$_n$.v} \texttt{> Makefile}
-\end{quotation}
-
-The resulted {\tt Makefile} has a target {\tt depend} which computes the
-dependencies and puts them in a separate file {\tt .depend}, which is
-included by the {\tt Makefile}. 
-Therefore, you should create such a file before the first invocation
-of make. You can for instance use the command 
-
-\begin{quotation}
-\texttt{\% touch .depend}
-\end{quotation}
-
-Then, to initialize or update the modules dependencies, type in:
+Arguments are explain by \texttt{\% coq\_makefile --help}.  They can be directly
+written in the command line but it is recommended to write them in a file (called
+for example {\tt Make}) and then call {\tt coq\_makefile -f Make -o
+  Makefile}. That means options are in {\tt Make} file and output is {\tt
+  Makefile} This way, {\tt Makefile} will be automatically regenerated if
+something changes in {\tt Make}.
 
+The first time you use this tool, you may be happy with:
 \begin{quotation}
-\texttt{\% make depend}
+\texttt{\% \{ echo '-R .} {\em MyFancyLib} \texttt{' ; find -name '*.v' -print \} >
+  Make \&\& coq\_makefile -f Make -o Makefile}
 \end{quotation}
 
-There is a target {\tt all} to compile all the files {\em file$_1$
-\dots\ file$_n$}, and a generic target to produce a {\tt .vo} file from
-the corresponding {\tt .v} file (so you can do {\tt make} {\em file}{\tt.vo}
-to compile the file {\em file}{\tt.v}).
-
-{\tt coq\_makefile} can also handle the case of ML files and
-subdirectories. For more options type
-
-\begin{quotation}
-\texttt{\% coq\_makefile --help}
-\end{quotation}
+To customize things afterwards, remember:
+\begin{itemize}
+\item Coq files must end in {\tt .v}, caml modules in {\tt .ml4} if they
+  require camlp preproccessing (and in {\tt .ml} otherwise), and caml module signatures in {\tt
+    .mli}.
+\item If you give a directory directly as argument, it is because you provide a
+  Makefile for it in it.
+\item {\tt -R} option is for Coq, {\tt -I} for caml. The same directory can
+  ``included'' by both.
+  Using {\tt -R} option gives a right logical path and a correct installation
+  emplacement to your coq files.
+\item If your files depend on an external library that isn't install somewhere
+  looked by coqc, use {\tt OTHERFLAGS = '-R path/to/lib lib\_name'} option in your {\tt
+    Make} but don't do {\tt -R \dots} directly, the {\em make clean} command would
+  erase it!
+\end{itemize}
 
 \Warning To compile a project containing \ocaml{} files you must keep
 the sources of \Coq{} somewhere and have an environment variable named
 \texttt{COQTOP} that points to that directory.
 
-% \section{{\sf Coq\_SearchIsos}: information retrieval in a \Coq\ proofs
-% library}
-% \label{coqsearchisos}
-% \index{Coq\_SearchIsos@{\sf Coq\_SearchIsos}}
-
-% In the \Coq\ distribution, there is also a separated and independent tool,
-% called {\sf Coq\_SearchIsos}, which allows the search in accordance with {\tt
-% SearchIsos}\index{SearchIsos@{\tt SearchIsos}} (see Section~\ref{searchisos})
-% in a \Coq\ proofs library. More precisely, this program begins, once launched
-% by {\tt coqtop -searchisos}\index{coqtopsearchisos@{\tt
-% coqtop -searchisos}}, loading lightly (by using specifications functions)
-% all the \Coq\ objects files ({\tt .vo}) accessible by the {\tt LoadPath} (see
-% Section~\ref{loadpath}). Next, a prompt appears and four commands are then
-% available:
-
-% \begin{description}
-% \item [{\tt SearchIsos}]\ \\
-%   Scans the fixed context.
-% \item [{\tt Time}]\index{Time@{\tt Time}}\ \\
-%   Turns on the Time Search Display mode (see Section~\ref{time}).
-% \item [{\tt Untime}]\index{Untime@{\tt Untime}}\ \\
-%   Turns off the Time Search Display mode (see Section~\ref{time}).
-% \item [{\tt Quit}]\index{Quit@{\tt Quit}}\ \\
-%   Ends the {\tt coqtop -searchisos} session.
-% \end{description}
-
-% When running {\tt coqtop -searchisos} you can use the two options:
-
-% \begin{description}
-% \item[{\tt -opt}]\ \\
-%   Runs the native-code version of {\sf Coq\_SearchIsos}.
-
-% \item[{\tt -image} {\em file}]\ \\
-%   This option sets the binary image to be used to be {\em file}
-%   instead of the standard one. Not of general use.
-% \end{description}
-
-
 \section[Documenting \Coq\ files with coqdoc]{Documenting \Coq\ files with coqdoc\label{coqdoc}
 \index{Coqdoc@{\sf coqdoc}}}
 
@@ -200,8 +157,8 @@ have been completely produced with {\tt coq-tex}.
 \subsection{The \Coq\ Emacs mode}
 
 \Coq\ comes with a Major mode for \emacs, {\tt coq.el}. This mode provides
-syntax highlighting (assuming your \emacs\ library provides
-{\tt hilit19.el}) and also a rudimentary indentation facility
+syntax highlighting
+and also a rudimentary indentation facility
 in the style of the Caml \emacs\ mode.
 
 Add the following lines to your \verb!.emacs! file:
@@ -232,7 +189,7 @@ Instructions to use it are contained in this file.
 \subsection[Proof General]{Proof General\index{Proof General}}
 
 Proof General is a generic interface for proof assistants based on
-Emacs (or XEmacs). The main idea is that the \Coq\ commands you are
+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. 
 Thus you don't need to copy-paste the \Coq\ material from your files
@@ -264,8 +221,6 @@ There are man pages for the commands {\tt coqdep}, {\tt gallina} and
 \RefManCutCommand{ENDREFMAN=\thepage}
 %END LATEX
 
-% $Id: RefMan-uti.tex 11975 2009-03-14 11:29:36Z letouzey $
-
 %%% Local Variables: 
 %%% mode: latex
 %%% TeX-master: t
diff --git a/doc/refman/Reference-Manual.tex b/doc/refman/Reference-Manual.tex
index b0ada528..cc42c2ef 100644
--- a/doc/refman/Reference-Manual.tex
+++ b/doc/refman/Reference-Manual.tex
@@ -148,4 +148,3 @@ Options A and B of the licence are {\em not} elected.}
 \end{document}
 
 
-% $Id: Reference-Manual.tex 14090 2011-05-03 13:34:16Z pboutill $ 
diff --git a/doc/refman/Setoid.tex b/doc/refman/Setoid.tex
index 20c8c02b..8e1bb10c 100644
--- a/doc/refman/Setoid.tex
+++ b/doc/refman/Setoid.tex
@@ -710,5 +710,4 @@ using the command \texttt{Typeclasses Opaque} (see \S \ref{TypeclassesTransparen
 %%% Local Variables: 
 %%% mode: latex
 %%% TeX-master: "Reference-Manual"
-%%% compile-command: "make -C ../.. -f Makefile.stage3 doc/refman/Reference-Manual.pdf"
 %%% End: 
diff --git a/doc/refman/biblio.bib b/doc/refman/biblio.bib
index f93b66f9..192a9699 100644
--- a/doc/refman/biblio.bib
+++ b/doc/refman/biblio.bib
@@ -1246,6 +1246,19 @@ Languages},
     publisher = {}
 }
 
+@article{LeeWerner11,
+  author    = {Gyesik Lee and
+               Benjamin Werner},
+  title     = {Proof-irrelevant model of {CC} with predicative induction
+               and judgmental equality},
+  journal   = {Logical Methods in Computer Science},
+  volume    = {7},
+  number    = {4},
+  year      = {2011},
+  ee        = {http://dx.doi.org/10.2168/LMCS-7(4:5)2011},
+  bibsource = {DBLP, http://dblp.uni-trier.de}
+}
+
 @Comment{cross-references, must be at end}
 
 @Book{Bastad92,