Merge branch 'v8.5'

3 files changed, 231 insertions, 107 deletions

diff --git a/doc/refman/RefMan-com.tex b/doc/refman/RefMan-com.tex
index 8bb1cc331b..6f85849888 100644
--- a/doc/refman/RefMan-com.tex
+++ b/doc/refman/RefMan-com.tex
@@ -5,9 +5,9 @@
 
 There are three \Coq~commands: 
 \begin{itemize}
-\item {\tt coqtop}: The \Coq\ toplevel (interactive mode) ; 
-\item {\tt coqc} : The \Coq\ compiler (batch compilation).
-\item {\tt coqchk} : The \Coq\ checker (validation of compiled libraries)
+\item {\tt coqtop}: the \Coq\ toplevel (interactive mode);
+\item {\tt coqc}: the \Coq\ compiler (batch compilation);
+\item {\tt coqchk}: the \Coq\ checker (validation of compiled libraries).
 \end{itemize}
 The options are (basically) the same for the first two commands, and
 roughly described below. You can also look at the \verb!man! pages of
@@ -39,11 +39,10 @@ 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
 compile it into a {\em file}{\tt .vo} file (See ~\ref{compiled}).
 
-\Warning The name {\em file} must be a regular {\Coq} identifier, as
-defined in the Section~\ref{lexical}. It
-must only contain letters, digits or underscores
-(\_). Thus it can be \verb+/bar/foo/toto.v+ but cannot be
-\verb+/bar/foo/to-to.v+.
+\Warning The name {\em file} should be a regular {\Coq} identifier, as
+defined in Section~\ref{lexical}. It should contain only letters, digits
+or underscores (\_). For instance, \verb+/bar/foo/toto.v+ is valid, but
+\verb+/bar/foo/to-to.v+ is invalid.
 
 \section[Customization]{Customization at launch time}
 
@@ -64,7 +63,7 @@ directories to the load path of \Coq.
 It is possible to skip the loading of the resource file with the
 option \verb:-q:.
 
-\section{By environment variables\label{EnvVariables}
+\subsection{By environment variables\label{EnvVariables}
 \index{Environment variables}\label{envars}}
 
 Load path can be specified to the \Coq\ system by setting up
@@ -93,13 +92,13 @@ The following command-line options are recognized by the commands {\tt
   coqc} and {\tt coqtop}, unless stated otherwise:
 
 \begin{description}
-\item[{\tt -I} {\em directory}, {\tt -include} {\em directory}]\
+\item[{\tt -I} {\em directory}, {\tt -include} {\em directory}]\ %
 
-Add physical path {\em directory} to the {\ocaml} loadpath.
+  Add physical path {\em directory} to the {\ocaml} loadpath.
 
   \SeeAlso Section~\ref{Libraries} and the command {\tt Declare ML Module} Section \ref{compiled}.
 
-\item[\texttt{-Q} \emph{directory} {\dirpath}]\
+\item[{\tt -Q} {\em directory} {\dirpath}]\ %
 
   Add physical path \emph{directory} to the list of directories where
   {\Coq} looks for a file and bind it to the the logical directory
@@ -109,147 +108,184 @@ Add physical path {\em directory} to the {\ocaml} loadpath.
 
   \SeeAlso Section~\ref{Libraries}.
 
-\item[{\tt -R} {\em directory} {\dirpath}]\
+\item[{\tt -R} {\em directory} {\dirpath}]\ %
 
   Do as \texttt{-Q} \emph{directory} {\dirpath} but make the
   subdirectory structure of \emph{directory} recursively visible so
   that the recursive contents of physical \emph{directory} is available
   from {\Coq} using short or partially qualified names.
-  
+
   \SeeAlso Section~\ref{Libraries}.
 
-\item[{\tt -top} {\dirpath}, {\tt -notop}]\ 
+\item[{\tt -top} {\dirpath}]\ %
+
+  Set the toplevel module name to {\dirpath} instead of {\tt Top}. Not
+  valid for {\tt coqc} as the toplevel module name is inferred from the
+  name of the output file.
+
+\item[{\tt -notop}]\ %
+
+  Use the empty logical path for the toplevel module name instead of {\tt
+    Top}. Not valid for {\tt coqc} as the toplevel module name is
+  inferred from the name of the output file.
+
+\item[{\tt -exclude-dir} {\em directory}]\ %
 
-  This sets the toplevel module name to {\dirpath}/the empty logical path instead
-  of {\tt Top}. Not valid for {\tt coqc}.
+  Exclude any subdirectory named {\em directory} while
+  processing options such as {\tt -R} and {\tt -Q}. By default, only the
+  conventional version control management directories named {\tt CVS} and
+  {\tt \_darcs} are excluded.
 
-\item[{\tt -exclude-dir} {\em subdirectory}]\ 
+\item[{\tt -nois}]\ %
 
-  This tells to exclude any subdirectory named {\em subdirectory}
-  while processing option {\tt -R}. Without this option only the
-  conventional version control management subdirectories named {\tt
-  CVS} and {\tt \_darcs} are excluded.
+  Start from an empty state instead of loading the {\tt Init.Prelude}
+  module.
 
-\item[{\tt -nois}]\ 
+\item[{\tt -init-file} {\em file}]\ %
 
-  Cause \Coq~to begin with an empty state.
+  Load {\em file} as the resource file instead of loading the default
+  resource file from the standard configuration directories.
 
-\item[{\tt -init-file} {\em file}, {\tt -q}]\ 
+\item[{\tt -q}]\ %
 
-  Take {\em file} as the resource file. /
-  Cause \Coq~not to load the resource file.
+  Do not to load the default resource file.
 
-\item[{\tt -load-ml-source} {\em file}]\ 
+\item[{\tt -load-ml-source} {\em file}]\ %
 
   Load the {\ocaml} source file {\em file}.
 
-\item[{\tt -load-ml-object} {\em file}]\ 
+\item[{\tt -load-ml-object} {\em file}]\ %
 
   Load the {\ocaml} object file {\em file}.
 
-\item[{\tt -l[v]} {\em file}, {\tt -load-vernac-source[-verbose]} {\em file}]\ 
+\item[{\tt -l} {\em file}, {\tt -load-vernac-source} {\em file}]\ %
+
+  Load and execute the {\Coq} script from {\em file.v}.
+
+\item[{\tt -lv} {\em file}, {\tt -load-vernac-source-verbose} {\em
+    file}]\ %
+
+  Load and execute the {\Coq} script from {\em file.v}.
+  Output its content on the standard input as it is executed.
+
+\item[{\tt -load-vernac-object} {\dirpath}]\ %
+
+  Load \Coq~compiled library {\dirpath}. This is equivalent to running
+  {\tt Require} {\dirpath}.
 
-  Load \Coq~file {\em file}{\tt .v} optionally with copy it contents on the
-  standard input.
+\item[{\tt -require} {\dirpath}]\ %
 
-\item[{\tt -load-vernac-object} {\em path}]\ 
+  Load \Coq~compiled library {\dirpath} and import it. This is equivalent
+  to running {\tt Require Import} {\dirpath}.
 
-  Load \Coq~compiled library {\em path} (equivalent to {\tt Require} {\em path}).
+\item[{\tt -batch}]\ %
 
-\item[{\tt -require} {\em path}]\ 
+  Exit just after argument parsing. Available for {\tt coqtop} only.
 
-  Load \Coq~compiled library {\em path} and import it (equivalent to {\tt
-    Require Import} {\em path}).
+\item[{\tt -compile} {\em file.v}]\ %
 
-\item[{\tt -compile} {\em file.v},{\tt -compile-verbose} {\em file.v}, {\tt -batch}]\ 
+  Compile file {\em file.v} into {\em file.vo}. This options imply {\tt
+    -batch} (exit just after argument parsing). It is available only
+  for {\tt coqtop}, as this behavior is the purpose of {\tt coqc}.
 
-  {\tt coqtop} options only used internally by {\tt coqc}.
+\item[{\tt -compile-verbose} {\em file.v}]\ %
 
-  This compiles file {\em file.v} into {\em file}{\tt .vo} without/with a
-  copy of the contents of the file on standard input.  This option implies options
-  {\tt -batch} (exit just after arguments parsing). It is only
-  available for {\tt coqtop}.
+  Same as {\tt -compile} but also output the content of {\em file.v} as
+  it is compiled.
 
-\item[{\tt -verbose}]\ 
+\item[{\tt -verbose}]\ %
 
-  This option is only for {\tt coqc}. It tells to compile the file with
-  a copy of its contents on standard input.
+  Output the content of the input file as it is compiled. This option is
+  available for {\tt coqc} only; it is the counterpart of {\tt
+    -compile-verbose}.
 
 %Mostly unused in the code
-%\item[{\tt -debug}]\ 
+%\item[{\tt -debug}]\ %
 %
 %  Switch on the debug flag.
 
-\item[{\tt -with-geoproof} (yes|no)]\ 
+\item[{\tt -with-geoproof} (yes|no)]\ %
 
-  Activate or not special functions for Geoproof within {\CoqIDE} (default is yes).
+  Enable or not special functions for Geoproof within {\CoqIDE} (default
+  is yes).
 
-\item[{\tt -color} (on|off|auto)]\
+\item[{\tt -color} (on|off|auto)]\ %
 
-  Activate or not the coloring of output of {\tt coqtop}. The default, auto,
-  means that {\tt coqtop} will dynamically decide whether to activate it
-  depending if the output channels of {\tt coqtop} can handle ANSI styles.
+  Enable or not the coloring of output of {\tt coqtop}. Default is auto,
+  meaning that {\tt coqtop} dynamically decides, depending on whether the
+  output channel supports ANSI escape sequences.
 
-\item[{\tt -beautify}]\ 
+\item[{\tt -beautify}]\ %
 
-  While compiling {\em file}, pretty prints each command just after having parsing
-  it in {\em file}{\tt .beautified} in order to get old-fashion
-  syntax/definitions/notations.
+  Pretty-print each command to {\em file.beautified} when compiling {\em
+    file.v}, in order to get old-fashioned syntax/definitions/notations.
 
-\item[{\tt -emacs}, {\tt -ide-slave}]\ 
+\item[{\tt -emacs}, {\tt -ide-slave}]\ %
 
-  Start a special main loop to communicate with ide.
+  Start a special toplevel to communicate with a specific IDE.
 
-\item[{\tt -impredicative-set}]\ 
+\item[{\tt -impredicative-set}]\ %
 
   Change the logical theory of {\Coq} by declaring the sort {\tt Set}
-  impredicative; warning: this is known to be inconsistent with
+  impredicative. Warning: this is known to be inconsistent with
   some standard axioms of classical mathematics such as the functional
-  axiom of choice or the principle of description
+  axiom of choice or the principle of description.
 
-\item[{\tt -type-in-type}]\
+\item[{\tt -type-in-type}]\ %
 
-  This collapses the universe hierarchy of {\Coq} making the logic inconsistent.
+  Collapse the universe hierarchy of {\Coq}. Warning: this makes the
+  logic inconsistent.
 
-\item[{\tt -compat} {\em version}] \mbox{}
+\item[{\tt -compat} {\em version}]\ %
 
-  Attempt to maintain some of the incompatible changes in their {\em version}
-  behavior.
+  Attempt to maintain some backward-compatibility with a previous version.
 
-\item[{\tt -dump-glob} {\em file}]\ 
+\item[{\tt -dump-glob} {\em file}]\ %
 
-  This dumps references for global names in file {\em file}
-  (to be used by coqdoc, see~\ref{coqdoc})
+  Dump references for global names in file {\em file} (to be used
+  by {\tt coqdoc}, see~\ref{coqdoc}). By default, if {\em file.v} is being
+  compiled, {\em file.glob} is used.
 
-\item[{\tt -no-hash-consing}] \mbox{}
+\item[{\tt -no-glob}]\ %
 
-\item[{\tt -image} {\em file}]\ 
+  Disable the dumping of references for global names.
 
-  This option sets the binary image to be used by {\tt coqc} to be {\em file}
+%\item[{\tt -no-hash-consing}]\ %
+
+\item[{\tt -image} {\em file}]\ %
+
+  Set the binary image to be used by {\tt coqc} to be {\em file}
   instead of the standard one. Not of general use.
 
-\item[{\tt -bindir} {\em directory}]\ 
+\item[{\tt -bindir} {\em directory}]\ %
+
+  Set the directory containing {\Coq} binaries to be used by {\tt coqc}.
+  It is equivalent to doing \texttt{export COQBIN=}{\em directory} before
+  launching {\tt coqc}.
+
+\item[{\tt -where}]\ %
+
+  Print the location of \Coq's standard library and exit.
 
-  Set for {\tt coqc} the directory containing \Coq\ binaries.
-  It is equivalent to do \texttt{export COQBIN=}{\em directory}
-  before launching {\tt coqc}.
+\item[{\tt -config}]\ %
 
-\item[{\tt -where}, {\tt -config}, {\tt -filteropts}]\ 
+  Print the locations of \Coq's binaries, dependencies, and libraries, then exit.
 
-  Print the \Coq's standard library location or \Coq's binaries, dependencies,
-  libraries locations or the list of command line arguments that {\tt coqtop} has
-  recognize as options and exit.
+\item[{\tt -filteropts}]\ %
 
-\item[{\tt -v}]\ 
+  Print the list of command line arguments that {\tt coqtop} has
+  recognized as options and exit.
 
-  Print the \Coq's version and exit.
+\item[{\tt -v}]\ %
 
-\item[{\tt -list-tags}]\
+  Print \Coq's version and exit.
 
-  Print the highlight tags known by \Coq as well as their currently associated
-  color.
+\item[{\tt -list-tags}]\ %
 
-\item[{\tt -h}, {\tt --help}]\ 
+  Print the highlight tags known by {\Coq} as well as their currently associated
+  color and exit.
+
+\item[{\tt -h}, {\tt --help}]\ %
 
   Print a short usage and exit.
 
@@ -293,18 +329,21 @@ Command-line options {\tt -I}, {\tt -R}, {\tt -where} and
 {\tt -impredicative-set} are supported by {\tt coqchk} and have the
 same meaning as for {\tt coqtop}. Extra options are:
 \begin{description}
-\item[{\tt -norec} $module$]\ 
+\item[{\tt -norec} {\em module}]\ %
+
+  Check {\em module} but do not check its dependencies.
 
-  Check $module$ but do not force check of its dependencies.
-\item[{\tt -admit} $module$] \
+\item[{\tt -admit} {\em module}]\ %
 
-  Do not check $module$ and any of its dependencies, unless
+  Do not check {\em module} and any of its dependencies, unless
   explicitly required.
-\item[{\tt -o}]\ 
+
+\item[{\tt -o}]\ %
 
   At exit, print a summary about the context. List the names of all
   assumptions and variables (constants without body).
-\item[{\tt -silent}]\ 
+
+\item[{\tt -silent}]\ %
 
   Do not write progress information in standard output.
 \end{description}
diff --git a/doc/refman/RefMan-lib.tex b/doc/refman/RefMan-lib.tex
index 7227f4b7b6..4ebb484e7c 100644
--- a/doc/refman/RefMan-lib.tex
+++ b/doc/refman/RefMan-lib.tex
@@ -17,10 +17,11 @@ The \Coq\ library is structured into two parts:
 
 In addition, user-provided libraries or developments are provided by
 \Coq\ users' community. These libraries and developments are available
-for download at \texttt{http://coq.inria.fr} (see
+for download at \url{http://coq.inria.fr} (see
 Section~\ref{Contributions}).
 
-The chapter briefly reviews the \Coq\ libraries.
+The chapter briefly reviews the \Coq\ libraries whose contents can
+also be browsed at \url{http://coq.inria.fr/stdlib}.
 
 \section[The basic library]{The basic library\label{Prelude}}
 
@@ -799,7 +800,9 @@ At the end, it defines data-types at the {\Type} level.
 \subsection{Tactics}
 
 A few tactics defined at the user level are provided in the initial
-state\footnote{This is in module {\tt Tactics.v}}.
+state\footnote{This is in module {\tt Tactics.v}}. They are listed at
+\url{http://coq.inria.fr/stdlib} (paragraph {\tt Init}, link {\tt
+  Tactics}).
 
 \section{The standard library}
 
@@ -842,7 +845,7 @@ Chapter~\ref{Other-commands}).
 The different modules of the \Coq\ standard library are described in the
 additional document \verb!Library.dvi!. They are also accessible on the WWW
 through the \Coq\ homepage
-\footnote{\texttt{http://coq.inria.fr}}.
+\footnote{\url{http://coq.inria.fr}}.
 
 \subsection[Notations for integer arithmetics]{Notations for integer arithmetics\index{Arithmetical notations}}
 
@@ -1035,7 +1038,7 @@ intros; split_Rmult.
 
 \end{itemize}
 
-All this tactics has been written with the tactic language Ltac
+These tactics has been written with the tactic language Ltac
 described in Chapter~\ref{TacticLanguage}.
 
 \begin{coq_eval}
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index f268d82764..815594d8e9 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -864,16 +864,17 @@ introduction pattern~$p$:
   expects the product to be over an inductive type
   whose number of constructors is $n$ (or more generally over a type
   of conclusion an inductive type built from $n$ constructors,
-  e.g. {\tt C -> A\textbackslash/B if $n=2$}): it destructs the introduced
+  e.g. {\tt C -> A\textbackslash/B} with $n=2$ since {\tt
+    A\textbackslash/B} has 2 constructors): it destructs the introduced
   hypothesis as {\tt destruct} (see Section~\ref{destruct}) would and
   applies on each generated subgoal the corresponding tactic;
   \texttt{intros}~$p_{i1}$ {\ldots} $p_{im_i}$; if the disjunctive
-  pattern is part of a sequence of patterns and is not the last
-  pattern of the sequence, then {\Coq} completes the pattern so that all
-  the argument of the constructors of the inductive type are
-  introduced (for instance, the list of patterns {\tt [$\;$|$\;$] H}
-  applied on goal {\tt forall x:nat, x=0 -> 0=x} behaves the same as
-  the list of patterns {\tt [$\,$|$\,$?$\,$] H});
+  pattern is part of a sequence of patterns, then {\Coq} completes the
+  pattern so that all the arguments of the constructors of the
+  inductive type are introduced (for instance, the list of patterns
+  {\tt [$\;$|$\;$] H} applied on goal {\tt forall x:nat, x=0 -> 0=x}
+  behaves the same as the list of patterns {\tt [$\,$|$\,$?$\,$] H},
+  up to one exception explained in the Remark below);
 \item introduction over a conjunction of patterns {\tt ($p_1$, \ldots,
   $p_n$)} expects the goal to be a product over an inductive type $I$ with a
   single constructor that itself has at least $n$ arguments: it
@@ -887,10 +888,10 @@ introduction pattern~$p$:
   {\tt ($p_1$,(\ldots,(\dots,$p_n$)\ldots))}; it expects the
   hypothesis to be a sequence of right-associative binary inductive
   constructors such as {\tt conj} or {\tt ex\_intro}; for instance, an
-  hypothesis with type {\tt A\verb|/\|exists x, B\verb|/\|C\verb|/\|D} can be
+  hypothesis with type {\tt A\verb|/\|(exists x, B\verb|/\|C\verb|/\|D)} can be
   introduced via pattern {\tt (a \& x \& b \& c \& d)};
 \item if the product is over an equality type, then a pattern of the
-  form {\tt [=$p_{1}$ \dots\ $p_n$]} applies either {\tt injection}
+  form {\tt [= $p_{1}$ \dots\ $p_n$]} applies either {\tt injection}
   (see Section~\ref{injection}) or {\tt discriminate} (see
   Section~\ref{discriminate}) instead of {\tt destruct}; if {\tt
     injection} is applicable, the patterns $p_1$, \ldots, $p_n$ are
@@ -950,6 +951,7 @@ Abort.
 
 \Rem {\tt intros $p_1~\ldots~p_n$} is not fully equivalent to
 \texttt{intros $p_1$;\ldots; intros $p_n$} for the following reasons:
+\label{bracketing-last}
 \begin{itemize}
 \item A wildcard pattern never succeeds when applied isolated on a
   dependent product, while it succeeds as part of a list of
@@ -971,6 +973,13 @@ Show 2.
 
 \end{itemize}
 
+This later behavior can be avoided by setting the following option:
+
+\begin{quote}
+\optindex{Bracketing Last Introduction Pattern}
+{\tt Set Bracketing Last Introduction Pattern}
+\end{quote}
+
 \subsection{\tt clear \ident}
 \tacindex{clear}
 \label{clear}
@@ -1459,6 +1468,24 @@ a hypothesis or in the body or the type of a local definition.
 
 \end{Variants}
 
+\subsection{\tt admit}
+\tacindex{admit}
+\tacindex{give\_up}
+\label{admit}
+
+The {\tt admit} tactic allows temporarily skipping a subgoal so as to
+progress further in the rest of the proof.  A proof containing
+admitted goals cannot be closed with {\tt Qed} but only with
+{\tt Admitted}.
+
+\begin{Variants}
+
+  \item {\tt give\_up}
+
+    Synonym of {\tt admit}.
+
+\end{Variants}
+
 \subsection{\tt absurd \term}
 \tacindex{absurd}
 \label{absurd}
@@ -4113,6 +4140,7 @@ The tactic {\tt exists (n // m)} did not fail. The hole was solved by
 
 \subsection{\tt tauto}
 \tacindex{tauto}
+\tacindex{dtauto}
 \label{tauto}
 
 This tactic implements a decision procedure for intuitionistic propositional
@@ -4161,8 +4189,21 @@ Abort.
 because \verb=(forall x:nat, ~ A -> P x)= cannot be treated as atomic and an
 instantiation of \verb=x= is necessary.
 
+\begin{Variants}
+
+\item {\tt dtauto}
+
+  While {\tt tauto} recognizes inductively defined connectives
+  isomorphic to the standard connective {\tt and}, {\tt prod}, {\tt
+    or}, {\tt sum}, {\tt False}, {\tt Empty\_set}, {\tt unit}, {\tt
+    True}, {\tt dtauto} recognizes also all inductive types with
+  one constructors and no indices, i.e. record-style connectives.
+
+\end{Variants}
+
 \subsection{\tt intuition \tac}
 \tacindex{intuition}
+\tacindex{dintuition}
 \label{intuition}
 
 The tactic \texttt{intuition} takes advantage of the search-tree built
@@ -4195,8 +4236,49 @@ incompatibilities.
 \item {\tt intuition}
 
   Is equivalent to {\tt intuition auto with *}.
+
+\item {\tt dintuition}
+
+  While {\tt intuition} recognizes inductively defined connectives
+  isomorphic to the standard connective {\tt and}, {\tt prod}, {\tt
+    or}, {\tt sum}, {\tt False}, {\tt Empty\_set}, {\tt unit}, {\tt
+    True}, {\tt dintuition} recognizes also all inductive types with
+  one constructors and no indices, i.e. record-style connectives.
+
 \end{Variants}
 
+\optindex{Intuition Negation Unfolding}
+\optindex{Intuition Iff Unfolding}
+
+Some aspects of the tactic {\tt intuition} can be
+controlled using options. To avoid that inner negations which do not
+need to be unfolded are unfolded, use:
+
+\begin{quote}
+{\tt Unset Intuition Negation Unfolding}
+\end{quote}
+
+To do that all negations of the goal are unfolded even inner ones
+(this is the default), use:
+
+\begin{quote}
+{\tt Set Intuition Negation Unfolding}
+\end{quote}
+
+To avoid that inner occurrence of {\tt iff} which do not need to be
+unfolded are unfolded (this is the default), use:
+
+\begin{quote}
+{\tt Unset Intuition Iff Unfolding}
+\end{quote}
+
+To do that all negations of the goal are unfolded even inner ones
+(this is the default), use:
+
+\begin{quote}
+{\tt Set Intuition Iff Unfolding}
+\end{quote}
+
 % En attente d'un moyen de valoriser les fichiers de demos
 %\SeeAlso file \texttt{contrib/Rocq/DEMOS/Demo\_tauto.v}