Merge branch 'v8.6'

7 files changed, 356 insertions, 40 deletions

diff --git a/doc/refman/Classes.tex b/doc/refman/Classes.tex
index e8ebb9f995..bd8ee450ef 100644
--- a/doc/refman/Classes.tex
+++ b/doc/refman/Classes.tex
@@ -9,10 +9,6 @@
 \aauthor{Matthieu Sozeau}
 \label{typeclasses}
 
-\begin{flushleft}
-  \em The status of Type Classes is experimental.
-\end{flushleft}
-
 This chapter presents a quick reference of the commands related to type
 classes. For an actual introduction to type classes, there is a
 description of the system \cite{sozeau08} and the literature on type
@@ -382,6 +378,70 @@ projections as instances. This is almost equivalent to {\tt Hint Resolve
 Declares variables according to the given binding context, which might
 use implicit generalization (see \ref{SectionContext}).
 
+\asubsection{\tt typeclasses eauto}
+\tacindex{typeclasses eauto}
+
+The {\tt typeclasses eauto} tactic uses a different resolution engine
+than {\tt eauto} and {\tt auto}. The main differences are the following:
+\begin{itemize}
+\item Contrary to {\tt eauto} and {\tt auto}, the resolution is done
+  entirely in the new proof engine (as of Coq v8.6), meaning that
+  backtracking is available among dependent subgoals, and shelving goals
+  is supported. {\tt typeclasses eauto} is a multi-goal tactic.
+  It analyses the dependencies between subgoals to avoid
+  backtracking on subgoals that are entirely independent.
+\item When called with no arguments, {\tt typeclasses eauto} uses the
+  {\tt typeclass\_instances} database by default (instead of {\tt
+    core}).
+  Dependent subgoals are automatically shelved, and shelved
+  goals can remain after resolution ends (following the behavior of
+  \Coq{} 8.5).
+
+  \emph{Note: } As of Coq 8.6, {\tt all:once (typeclasses eauto)}
+  faithfully mimicks what happens during typeclass resolution when it is
+  called during refinement/type-inference, except that \emph{only}
+  declared class subgoals are considered at the start of resolution
+  during type inference, while ``all'' can select non-class subgoals as
+  well. It might move to {\tt all:typeclasses eauto} in future versions
+  when the refinement engine will be able to backtrack.
+\item When called with specific databases (e.g. {\tt with}), {\tt
+    typeclasses eauto} allows shelved goals to remain at any point
+  during search and treat typeclasses goals like any other.
+\item The transparency information of databases is used consistently for
+  all hints declared in them. It is always used when calling the unifier.
+  When considering the local hypotheses, we use the transparent
+  state of the first hint database given. Using an empty database
+  (created with {\tt Create HintDb} for example) with 
+  unfoldable variables and constants as the first argument of
+  typeclasses eauto hence makes resolution with the local hypotheses use
+  full conversion during unification.
+\end{itemize}
+
+\begin{Variants}
+\item \label{depth} {\tt typeclasses eauto \zeroone{\num}}
+  \emph{Warning:} The semantics for the limit {\num} is different than
+  for {\tt auto}. By default, if no limit is given the search is
+  unbounded. Contrary to {\tt auto}, introduction steps ({\tt intro})
+  are counted, which might result in larger limits being necessary
+  when searching with {\tt typeclasses eauto} than {\tt auto}.
+  
+\item \label{with} {\tt typeclasses eauto with {\ident}$_1$ \ldots {\ident}$_n$}.
+  This variant runs resolution with the given hint databases. It treats
+  typeclass subgoals the same as other subgoals (no shelving of
+  non-typeclass goals in particular).
+\end{Variants}
+
+\asubsection{\tt autoapply {\term} with {\ident}}
+\tacindex{autoapply}
+
+The tactic {\tt autoapply} applies a term using the transparency
+information of the hint database {\ident}, and does \emph{no} typeclass
+resolution. This can be used in {\tt Hint Extern}'s for typeclass
+instances (in hint db {\tt typeclass\_instances}) to
+allow backtracking on the typeclass subgoals created by the lemma
+application, rather than doing type class resolution locally at the hint
+application time.
+
 \subsection{\tt Typeclasses Transparent, Opaque {\ident$_1$ \ldots \ident$_n$}}
 \comindex{Typeclasses Transparent}
 \comindex{Typeclasses Opaque}
@@ -400,20 +460,123 @@ abbreviate a type, like {\tt relation A := A -> A -> Prop}.
 
 This is equivalent to {\tt Hint Transparent,Opaque} {\ident} {\tt: typeclass\_instances}.
 
+\subsection{\tt Set Typeclasses Dependency Order}
+\optindex{Typeclasses Dependency Order}
+
+This option (on by default since 8.6) respects the dependency order between
+subgoals, meaning that subgoals which are depended on by other subgoals 
+come first, while the non-dependent subgoals were put before the
+dependent ones previously (Coq v8.5 and below). This can result in quite
+different performance behaviors of proof search.
+
+\subsection{\tt Set Typeclasses Filtered Unification}
+\optindex{Typeclasses Filtered Unification}
+
+This option, available since Coq 8.6 and off by default, switches the
+hint application procedure to a filter-then-unify strategy. To apply a
+hint, we first check that the goal \emph{matches} syntactically the
+inferred or specified pattern of the hint, and only then try to
+\emph{unify} the goal with the conclusion of the hint. This can
+drastically improve performance by calling unification less often,
+matching syntactic patterns being very quick. This also provides more
+control on the triggering of instances.  For example, forcing a constant
+to explicitely appear in the pattern will make it never apply on a goal
+where there is a hole in that place.
+
+\subsection{\tt Set Typeclasses Legacy Resolution}
+\optindex{Typeclasses Legacy Resolution}
+
+This option (off by default) uses the 8.5 implementation of resolution.
+Use for compatibility purposes only (porting and debugging).
+
+\subsection{\tt Set Typeclasses Module Eta}
+\optindex{Typeclasses Modulo Eta}
+
+This option allows eta-conversion for functions and records during
+unification of type-classes. This option is now unsupported in 8.6 with
+{\tt Typeclasses Filtered Unification} set, but still affects the
+default unification strategy, and the one used in {\tt Legacy
+  Resolution} mode. It is \emph{unset} by default. If {\tt Typeclasses
+  Filtered Unification} is set, this has no effect and unification will
+find solutions up-to eta conversion. Note however that syntactic
+pattern-matching is not up-to eta.
+
+\subsection{\tt Set Typeclasses Limit Intros}
+\optindex{Typeclasses Limit Intros}
+
+This option (on by default in Coq 8.6 and below) controls the ability to
+apply hints while avoiding (functional) eta-expansions in the generated
+proof term. It does so by allowing hints that conclude in a product to
+apply to a goal with a matching product directly, avoiding an
+introduction. \emph{Warning:} this can be expensive as it requires
+rebuilding hint clauses dynamically, and does not benefit from the
+invertibility status of the product introduction rule, resulting in
+potentially more expensive proof-search (i.e. more useless
+backtracking).
+
+\subsection{\tt Set Typeclass Resolution After Apply}
+\optindex{Typeclasses Resolution After Apply}
+\emph{Deprecated since 8.6}
+
+This option (off by default in Coq 8.6 and 8.5) controls the resolution
+of typeclass subgoals generated by the {\tt apply} tactic.
+
+\subsection{\tt Set Typeclass Resolution For Conversion}
+\optindex{Typeclasses Resolution For Conversion}
+
+This option (on by default) controls the use of typeclass resolution
+when a unification problem cannot be solved during
+elaboration/type-inference. With this option on, when a unification
+fails, typeclass resolution is tried before launching unification once again.
+
+\subsection{\tt Set Typeclasses Strict Resolution}
+\optindex{Typeclasses Strict Resolution}
+
+Typeclass declarations introduced when this option is set have a
+stricter resolution behavior (the option is off by default). When
+looking for unifications of a goal with an instance of this class, we
+``freeze'' all the existentials appearing in the goals, meaning that
+they are considered rigid during unification and cannot be instantiated.
+
+\subsection{\tt Set Typeclasses Unique Solutions}
+\optindex{Typeclasses Unique Solutions}
+
+When a typeclass resolution is launched we ensure that it has a single
+solution or fail. This ensures that the resolution is canonical, but can
+make proof search much more expensive.
+
+\subsection{\tt Set Typeclasses Unique Instances}
+\optindex{Typeclasses Unique Instances}
+
+Typeclass declarations introduced when this option is set have a
+more efficient resolution behavior (the option is off by default). When
+a solution to the typeclass goal of this class is found, we never
+backtrack on it, assuming that it is canonical.
+
 \subsection{\tt Typeclasses eauto := [debug] [dfs | bfs] [\emph{depth}]}
 \comindex{Typeclasses eauto}
 \label{TypeclassesEauto}
 
-This command allows customization of the type class resolution tactic,
-based on a variant of eauto. The flags semantics are:
+This command allows more global customization of the type class
+resolution tactic.
+The semantics of the options are:
 \begin{itemize}
 \item {\tt debug} In debug mode, the trace of successfully applied
   tactics is printed.
 \item {\tt dfs, bfs} This sets the search strategy to depth-first search
   (the default) or breadth-first search.
-\item {\emph{depth}} This sets the depth of the search (the default is 100).
+\item {\emph{depth}} This sets the depth limit of the search.
 \end{itemize}
 
+\subsection{\tt Set Typeclasses Debug [Verbosity {\num}]}
+\optindex{Typeclasses Debug}
+\optindex{Typeclasses Debug Verbosity}
+
+These options allow to see the resolution steps of typeclasses that are
+performed during search. The {\tt Debug} option is synonymous to 
+{\tt Debug Verbosity 1}, and {\tt Debug Verbosity 2} provides more
+information (tried tactics, shelving of goals, etc\ldots).
+
 \subsection{\tt Set Refine Instance Mode}
 \optindex{Refine Instance Mode}
 
diff --git a/doc/refman/RefMan-com.tex b/doc/refman/RefMan-com.tex
index 6f85849888..c1e552a5da 100644
--- a/doc/refman/RefMan-com.tex
+++ b/doc/refman/RefMan-com.tex
@@ -199,6 +199,12 @@ The following command-line options are recognized by the commands {\tt
   available for {\tt coqc} only; it is the counterpart of {\tt
     -compile-verbose}.
 
+  \item[{\tt -w} (all|none|w$_1$,\ldots,w$_n$)]\ %
+
+  Configure the display of warnings. This option expects {\tt all}, {\tt none}
+  or a comma-separated list of warning names or categories (see
+  Section~\ref{SetWarnings}).
+
 %Mostly unused in the code
 %\item[{\tt -debug}]\ %
 %
diff --git a/doc/refman/RefMan-ext.tex b/doc/refman/RefMan-ext.tex
index 51e881bff4..b475a5233c 100644
--- a/doc/refman/RefMan-ext.tex
+++ b/doc/refman/RefMan-ext.tex
@@ -1315,10 +1315,10 @@ command:
 \begin{quote}
 \tt Arguments {\qualid} \nelist{\possiblybracketedident}{}
 \end{quote}
-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.
+where the list of {\possiblybracketedident} is a prefix of the list of 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
@@ -1591,7 +1591,7 @@ Implicit arguments names can be redefined using the following syntax:
 {\tt Arguments {\qualid} \nelist{\name}{}  : rename}
 \end{quote}
 
-Without the {\tt rename} flag, {\tt Arguments} can be used to assert
+With the {\tt assert} flag, {\tt Arguments} can be used to assert
 that a given object has the expected number of arguments and that
 these arguments are named as expected.
 
@@ -1600,7 +1600,7 @@ these arguments are named as expected.
 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] _.
+Fail Arguments p [s t] _ [w] _ : assert.
 \end{coq_example}
 
 
diff --git a/doc/refman/RefMan-oth.tex b/doc/refman/RefMan-oth.tex
index 919e7b5cdc..56ce753cd6 100644
--- a/doc/refman/RefMan-oth.tex
+++ b/doc/refman/RefMan-oth.tex
@@ -914,6 +914,19 @@ This command turns off the normal displaying.
 \subsection[\tt Unset Silent.]{\tt Unset Silent.\optindex{Silent}}
 This command turns the normal display on.
 
+\subsection[\tt Set Warnings ``(\nterm{w}$_1$,\ldots,%
+  \nterm{w}$_n$)''.]{{\tt Set Warnings ``(\nterm{w}$_1$,\ldots,%
+  \nterm{w}$_n$)''}.\optindex{Warnings}}
+\label{SetWarnings}
+This command configures the display of warnings. It is experimental, and
+expects, between quotes, a comma-separated list of warning names or
+categories. Adding~\texttt{-} in front of a warning or category disables it,
+adding~\texttt{+} makes it an error. It is possible to use the special
+categories \texttt{all} and \texttt{default}, the latter containing the warnings
+enabled by default. The flags are interpreted from left to right, so in case of
+an overlap, the flags on the right have higher priority, meaning that
+\texttt{A,-A} is equivalent to \texttt{-A}.
+
 \subsection[\tt Set Search Output Name Only.]{\tt Set Search Output Name Only.\optindex{Search Output Name Only}
 \label{Search-Output-Name-Only}
 \index{Search Output Name Only mode}}
diff --git a/doc/refman/RefMan-pre.tex b/doc/refman/RefMan-pre.tex
index cb2ab5dc2f..f36969e821 100644
--- a/doc/refman/RefMan-pre.tex
+++ b/doc/refman/RefMan-pre.tex
@@ -1087,6 +1087,139 @@ Paris, January 2015, revised December 2015,\\
 Hugo Herbelin, Matthieu Sozeau and the {\Coq} development team\\
 \end{flushright}
 
+\section*{Credits: version 8.6}
+
+{\Coq} version 8.6 contains the result of refinements, stabilization of
+8.5's features and cleanups of the internals of the system. Over the
+year of (now time-based) development, about 450 bugs were resolved and
+over 100 contributions integrated. The main user visible changes are:
+\begin{itemize}
+\item A new, faster state-of-the-art universe constraint checker, by
+  Jacques-Henri Jourdan.
+\item In CoqIDE and other asynchronous interfaces, more fine-grained
+  asynchronous processing and error reporting by Enrico Tassi, making {\Coq}
+  capable of recovering from errors and continue processing the document.
+\item More access to the proof engine features from Ltac: goal
+  management primitives, range selectors and a {\tt typeclasses
+    eauto} engine handling multiple goals and multiple successes, by
+  Cyprien Mangin, Matthieu Sozeau and Arnaud Spiwack.
+\item Tactic behavior uniformization and specification, generalization
+  of intro-patterns by Hugo Herbelin and others.
+\item A brand new warning system allowing to control warnings, turn them
+  into errors or ignore them selectively by Maxime Dénès, Guillaume
+  Melquiond, Pierre-Marie Pédrot and others.
+\item Irrefutable patterns in abstractions, by Daniel de Rauglaudre.
+\item The {\tt ssreflect} subterm selection algorithm by Georges Gonthier and
+  Enrico Tassi is now accessible to tactic writers through the {\tt ssrmatching}
+  plugin.
+\item Integration of {\tt LtacProf}, a profiler for {\tt Ltac} by Jason
+  Gross, Paul Steckler, Enrico Tassi and Tobias Tebbi.
+\end{itemize}
+
+{\Coq} 8.6 also comes with a bunch of smaller-scale changes and
+improvements regarding the different components of the system. We shall
+only list a few of them.
+
+The {\tt iota} reduction flag is now a shorthand for {\tt match}, {\tt
+  fix} and {\tt cofix} flags controlling the corresponding reduction
+rules (by Hugo Herbelin and Maxime Dénès).
+
+Maxime Dénès maintained the native compilation machinery.
+
+Pierre-Marie Pédrot separated the Ltac code from general purpose
+tactics, and generalized and rationalized the handling of generic
+arguments, allowing to create new versions of Ltac more easily in the
+future.
+
+In patterns and terms, {\tt @}, abbreviations and notations are now
+interpreted the same way, by Hugo Herbelin.
+
+Name handling for universes has been improved by Pierre-Marie Pédrot and
+Matthieu Sozeau. The minimization algorithm has been improved by
+Matthieu Sozeau.
+
+The unifier has been improved by Hugo Herbelin and Matthieu Sozeau,
+fixing some incompatibilities introduced in Coq 8.5. Unification
+constraints can now be left floating around and be seen by the user
+thanks to a new option. The {\tt Keyed Unification} mode has been
+improved by Matthieu Sozeau. 
+
+The typeclass resolution engine and associated proof-search tactic have
+been reimplemented on top of the proof-engine monad, providing better
+integration in tactics, and new options have been introduced to control
+it, by Matthieu Sozeau with help from Théo Zimmermann.
+
+The efficiency of the whole system has been significantly improved
+thanks to contributions from Pierre-Marie Pédrot, Maxime Dénès and
+Matthieu Sozeau and performance issue tracking by Jason Gross and Paul
+Steckler.
+
+Standard library improvements by Jason Gross, Sébastien Hinderer, Pierre
+Letouzey and others.
+
+Emilio Jesús Gallego Arias contributed many cleanups and refactorings of
+the pretty-printing and user interface communication components.
+
+Frédéric Besson maintained the micromega tactic.
+
+The OPAM repository for {\Coq} packages has been maintained by Guillaume
+Claret, Guillaume Melquiond, Matthieu Sozeau, Enrico Tassi and others. A
+list of packages is now available at \url{https://coq.inria.fr/opam/www/}.
+
+Packaging tools and software development kits were prepared by Michael
+Soegtrop with the help of Maxime Dénès and Enrico Tassi for Windows, and
+Maxime Dénès and Matthieu Sozeau for MacOS X. Packages are now regularly
+built on the continuous integration server. {\Coq} now comes with a {\tt
+  META} file usable with {\tt ocamlfind}, contributed by Emilio Jesús
+Gallego Arias, Gregory Malecha, and Matthieu Sozeau.
+
+Matej Košík maintained and greatly improved the continuous integration
+setup and the testing of {\Coq} contributions. He also contributed many
+API improvement and code cleanups throughout the system.
+
+The contributors for this version are Bruno Barras, C.J. Bell, Yves
+Bertot, Frédéric Besson, Pierre Boutillier, Tej Chajed, Guillaume
+Claret, Xavier Clerc, Pierre Corbineau, Pierre Courtieu, Maxime Dénès,
+Ricky Elrod, Emilio Jesús Gallego Arias, Jason Gross, Hugo Herbelin,
+Sébastien Hinderer, Jacques-Henri Jourdan, Matej Kosik, Xavier Leroy,
+Pierre Letouzey, Gregory Malecha, Cyprien Mangin, Erik Martin-Dorel,
+Guillaume Melquiond, Clément Pit--Claudel, Pierre-Marie Pédrot, Daniel
+de Rauglaudre, Lionel Rieg, Gabriel Scherer, Thomas Sibut-Pinote,
+Matthieu Sozeau, Arnaud Spiwack, Paul Steckler, Enrico Tassi, Laurent
+Théry, Nickolai Zeldovich and Théo Zimmermann. The development process
+was coordinated by Hugo Herbelin and Matthieu Sozeau with the help of
+Maxime Dénès, who was also in charge of the release process.
+
+Many power users helped to improve the design of the new features via
+the bug tracker, the pull request system, the {\Coq} development mailing
+list or the coq-club mailing list. Special thanks to the users who
+contributed patches and intensive brain-storming and code reviews,
+starting with Cyril Cohen, Jason Gross, Robbert Krebbers, Jonathan
+Leivent, Xavier Leroy, Gregory Malecha, Clément Pit--Claudel, Gabriel
+Scherer and Beta Ziliani. It would however be impossible to mention
+exhaustively the names of everybody who to some extent influenced the
+development.
+
+Version 8.6 is the first release of {\Coq} developed on a time-based
+development cycle. Its development spanned 10 months from the release of
+{\Coq} 8.5 and was based on a public roadmap. To date, it contains more
+external contributions than any previous {\Coq} system. Code reviews
+were systematically done before integration of new features, with an
+important focus given to compatibility and performance issues, resulting
+in a hopefully more robust release than {\Coq} 8.5.
+
+Coq Enhancement Proposals (CEPs for short) were introduced by Enrico
+Tassi to provide more visibility and a discussion period on new
+features, they are publicly available \url{https://github.com/coq/ceps}.
+
+Started during this period, an effort is led by Yves Bertot and Maxime
+Dénès to put together a {\Coq} consortium.
+
+\begin{flushright}
+Paris, November 2016,\\
+Matthieu Sozeau and the {\Coq} development team\\
+\end{flushright}
+
 
 %new Makefile
 
diff --git a/doc/refman/RefMan-syn.tex b/doc/refman/RefMan-syn.tex
index 92107b750b..1fcc1c0df4 100644
--- a/doc/refman/RefMan-syn.tex
+++ b/doc/refman/RefMan-syn.tex
@@ -811,13 +811,13 @@ constant have to be interpreted in a given scope. The command is
 \begin{quote}
 {\tt Arguments} {\qualid} \nelist{\name {\tt \%}\scope}{}
 \end{quote}
-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}).
+where the list is a prefix of 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.
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index dd45feebc6..01dc1dec9b 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -263,6 +263,16 @@ Defined.
 
   This tactic behaves like {\tt refine}, but it does not shelve any
   subgoal. It does not perform any beta-reduction either.
+\item {\tt notypeclasses refine \term}\tacindex{notypeclasses refine}
+
+  This tactic behaves like {\tt refine} except it performs typechecking
+  without resolution of typeclasses.
+
+\item {\tt simple notypeclasses refine \term}\tacindex{simple
+    notypeclasses refine}
+
+  This tactic behaves like {\tt simple refine} except it performs typechecking
+  without resolution of typeclasses.
 \end{Variants}
 
 \subsection{\tt apply \term}
@@ -1278,7 +1288,7 @@ in the list of subgoals remaining to prove.
 
   In particular, \texttt{pose proof {\term} as {\ident}} behaves as
   \texttt{assert ({\ident} := {\term})} and \texttt{pose proof {\term}
-    as {\intropattern}\tacindex{pose proof}} is the same as applying
+    as {\intropattern}} is the same as applying
   the {\intropattern} to {\term}.
 
 \item \texttt{enough ({\ident} :\ {\form})}\tacindex{enough}
@@ -3493,8 +3503,7 @@ hints of the database named {\tt core}.
 
 \item {\tt auto with *}
 
-  Uses all existing hint databases, minus the special database
-  {\tt v62}. See Section~\ref{Hints-databases}
+  Uses all existing hint databases. See Section~\ref{Hints-databases}
 
 \item \texttt{auto using} \nterm{lemma}$_1$ {\tt ,} {\ldots} {\tt ,} \nterm{lemma}$_n$
 
@@ -3718,12 +3727,14 @@ command to add a hint to some databases \ident$_1$, \dots, \ident$_n$ is
 The {\hintdef} is one of the following expressions:
 
 \begin{itemize}
-\item {\tt Resolve \term}
+\item {\tt Resolve \term {\zeroone{{\tt |} \zeroone{\num} \zeroone{\pattern}}}}
   \comindex{Hint Resolve}
 
   This command adds {\tt simple apply {\term}} to the hint list
   with the head symbol of the type of \term. The cost of that hint is
-  the number of subgoals generated by {\tt simple apply {\term}}.
+  the number of subgoals generated by {\tt simple apply {\term}} or \num
+  if specified. The associated pattern is inferred from the conclusion
+  of the type of \term or the given \pattern if specified.
 %{\tt auto} actually uses a slightly modified variant of {\tt simple apply} with use_metas_eagerly_in_conv_on_closed_terms set to false
 
   In case the inferred type of \term\ does not start with a product
@@ -3907,7 +3918,7 @@ Abort.
 \comindex{Hint Cut}
 
   \textit{Warning:} these hints currently only apply to typeclass proof search and
-  the \texttt{typeclasses eauto} tactic.
+  the \texttt{typeclasses eauto} tactic (\ref{typeclasseseauto}).
 
   This command can be used to cut the proof-search tree according to a
   regular expression matching paths to be cut. The grammar for regular
@@ -3999,8 +4010,8 @@ Several hint databases are defined in the \Coq\ standard library.  The
 actual content of a database is the collection of the hints declared
 to belong to this database in each of the various modules currently
 loaded.  Especially, requiring new modules potentially extend a
-database. At {\Coq} startup, only the {\tt core} and {\tt v62}
-databases are non empty and can be used.
+database. At {\Coq} startup, only the {\tt core} database is non empty
+and can be used.
 
 \begin{description}
 
@@ -4035,18 +4046,8 @@ databases are non empty and can be used.
   from the \texttt{Classes} directory.
 \end{description}
 
-There is also a special database called {\tt v62}. It collects all
-hints that were declared in the versions of {\Coq} prior to version
-6.2.4 when the databases {\tt core}, {\tt arith}, and so on were
-introduced.  The purpose of the database {\tt v62} is to ensure
-compatibility with further versions of {\Coq} for developments done in
-versions prior to 6.2.4 ({\tt auto} being replaced by {\tt auto with v62}).
-The database {\tt v62} is intended not to be extended (!). It is not
-included in the hint databases list used in the {\tt auto with *} tactic.
-
-Furthermore, you are advised not to put your own hints in the
-{\tt core} database, but use one or several databases specific to your
-development.
+You are advised not to put your own hints in the {\tt core} database,
+but use one or several databases specific to your development.
 
 \subsection{\tt Remove Hints \term$_1$ \mbox{\dots} \term$_n$ :~ \ident$_1$
   \mbox{\dots} \ident$_m$}