From 5737c8a41782ee66e96f4e855b00e396a23e8479 Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Mon, 24 Oct 2016 17:39:06 +0200
Subject: Remove v62 from the refman.

---
 doc/refman/RefMan-tac.tex | 21 +++++----------------
 1 file changed, 5 insertions(+), 16 deletions(-)

(limited to 'doc/refman')

diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index 2da12c8d69..0aabaf6a87 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -3493,8 +3493,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$
 
@@ -3962,8 +3961,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}
 
@@ -3998,18 +3997,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$}
-- 
cgit v1.2.3


From e807f3407fb19f481dac332e7650eddfa9b5fd5d Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Fri, 14 Oct 2016 16:53:19 +0200
Subject: Documenting changes in typeclasses

---
 doc/refman/Classes.tex    | 144 +++++++++++++++++++++++++++++++++++++++++++---
 doc/refman/RefMan-tac.tex |   2 +-
 2 files changed, 138 insertions(+), 8 deletions(-)

(limited to 'doc/refman')

diff --git a/doc/refman/Classes.tex b/doc/refman/Classes.tex
index e8ebb9f995..e90621f046 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,55 @@ 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{typeclasseseauto}
+
+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.  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})
+  and will try to solve \emph{only} typeclass goals. Other subgoals are
+  automatically shelved and \emph{must be} resolved entirely when the
+  other typeclass subgoals are resolved.
+\item The transparency information of databases is used consistently.
+  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 does
+  not treat typeclass subgoals differently than others.
+\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 typeclasse
+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,18 +445,103 @@ 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 Module Eta}
+\optindex{Typeclasses Modulo Eta}
+
+This allows eta-conversion during unification of type-classes.
+
+\subsection{\tt Set Typeclasses Dependency Order}
+\optindex{Typeclasses Dependency Order}
+
+This option (now on by default) 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 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 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 eta-expansions in the proof term
+generated. It does so by allowing hints that conclude in an product to
+apply to a goal with a matching product directly, avoiding an
+introduction. \emph{Warning:} 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 more expensive
+proof-search (i.e. more useless backtracking).
+
+\subsection{\tt Set Typeclasses Filtered Unification}
+\optindex{Typeclasses Filtered Unification}
+
+This option, available since Coq 8.6, switches the hint application
+procedure to a filter-then-unify strategy. To apply a hint, we first
+check that it \emph{matches} syntactically the inferred 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 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 Refine Instance Mode}
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index dd45feebc6..c659e19e6b 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -3907,7 +3907,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
-- 
cgit v1.2.3


From 6ec511721efc9235f6c2fa922a21dcb9b041bbfd Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Thu, 3 Nov 2016 15:51:39 +0100
Subject: Document options of typeclasses (eauto)

With update after J. Gross comments
---
 doc/refman/Classes.tex | 85 +++++++++++++++++++++++++++++++-------------------
 1 file changed, 53 insertions(+), 32 deletions(-)

(limited to 'doc/refman')

diff --git a/doc/refman/Classes.tex b/doc/refman/Classes.tex
index e90621f046..144fc22b96 100644
--- a/doc/refman/Classes.tex
+++ b/doc/refman/Classes.tex
@@ -387,14 +387,16 @@ than {\tt eauto} and {\tt auto}. The main differences are the following:
 \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.  It analyses the dependencies between subgoals to avoid
+  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})
   and will try to solve \emph{only} typeclass goals. Other subgoals are
   automatically shelved and \emph{must be} resolved entirely when the
-  other typeclass subgoals are resolved.
-\item The transparency information of databases is used consistently.
+  other typeclass subgoals are resolved or the proof search will fail.
+\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 
@@ -412,8 +414,9 @@ than {\tt eauto} and {\tt auto}. The main differences are the following:
   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 does
-  not treat typeclass subgoals differently than others.
+  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}}
@@ -421,7 +424,7 @@ than {\tt eauto} and {\tt auto}. The main differences are the following:
 
 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 typeclasse
+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
@@ -445,50 +448,59 @@ 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 Module Eta}
-\optindex{Typeclasses Modulo Eta}
-
-This allows eta-conversion during unification of type-classes.
-
 \subsection{\tt Set Typeclasses Dependency Order}
 \optindex{Typeclasses Dependency Order}
 
-This option (now on by default) respects the dependency order between
+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 eta-expansions in the proof term
-generated. It does so by allowing hints that conclude in an product to
+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:} 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 more expensive
-proof-search (i.e. more useless backtracking).
-
-\subsection{\tt Set Typeclasses Filtered Unification}
-\optindex{Typeclasses Filtered Unification}
-
-This option, available since Coq 8.6, switches the hint application
-procedure to a filter-then-unify strategy. To apply a hint, we first
-check that it \emph{matches} syntactically the inferred 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.
+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}
@@ -544,6 +556,15 @@ The semantics of the options are:
 \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}
 
-- 
cgit v1.2.3


From d6fe6773c959493ed97108e1032b1bd8c1e78081 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Mon, 24 Oct 2016 18:18:33 +0200
Subject: Lets Hints/Instances take an optional pattern

In addition to a priority, cleanup the interfaces for passing this
information as well. The pattern, if given, takes priority over the
inferred one.
We only allow Existing Instances gr ... gr | pri. for now, without
pattern, as before.
Make the API compatible to 8.5 as well.
---
 doc/refman/Classes.tex    | 2 +-
 doc/refman/RefMan-tac.tex | 6 ++++--
 2 files changed, 5 insertions(+), 3 deletions(-)

(limited to 'doc/refman')

diff --git a/doc/refman/Classes.tex b/doc/refman/Classes.tex
index 144fc22b96..254fca28f7 100644
--- a/doc/refman/Classes.tex
+++ b/doc/refman/Classes.tex
@@ -379,7 +379,7 @@ Declares variables according to the given binding context, which might
 use implicit generalization (see \ref{SectionContext}).
 
 \asubsection{\tt typeclasses eauto}
-\tacindex{typeclasseseauto}
+\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:
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index c659e19e6b..0aa179d627 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -3718,12 +3718,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
-- 
cgit v1.2.3


From 98305374e2fdec4b64d7d086ddca0c4e812b178e Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Sat, 29 Oct 2016 11:51:38 +0200
Subject: typeclasses eauto Implem/doc of shelving strategy

Now [typeclasses eauto] mimicks what happens during resolution
faithfully, and the shelving behavior/requirements for a successful
proof-search are documented.
---
 doc/refman/Classes.tex | 13 ++++++++++++-
 1 file changed, 12 insertions(+), 1 deletion(-)

(limited to 'doc/refman')

diff --git a/doc/refman/Classes.tex b/doc/refman/Classes.tex
index 254fca28f7..d6a553e1a8 100644
--- a/doc/refman/Classes.tex
+++ b/doc/refman/Classes.tex
@@ -394,7 +394,18 @@ than {\tt eauto} and {\tt auto}. The main differences are the following:
   {\tt typeclass\_instances} database by default (instead of {\tt core})
   and will try to solve \emph{only} typeclass goals. Other subgoals are
   automatically shelved and \emph{must be} resolved entirely when the
-  other typeclass subgoals are resolved or the proof search will fail.
+  other typeclass subgoals are resolved or the proof search will fail
+  \emph{globally}, \emph{without} the possibility to find another
+  complete solution with no shelved subgoals.
+
+  \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. 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
-- 
cgit v1.2.3


From f6916774eea2ecc1262377cb14c2d494a0486358 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Sat, 29 Oct 2016 19:07:21 +0200
Subject: Do not shelve non-class subgoals but fail, it should

be the instance writer's responsibility to not generated non-dependent
non-class subgoals (otherwise we loose compatibility as shown in
e.g. MathClasses, which goes into loops because of unexpectedly
unconstrained goals). Reflect it in the doc.
---
 doc/refman/Classes.tex | 12 +++++++-----
 1 file changed, 7 insertions(+), 5 deletions(-)

(limited to 'doc/refman')

diff --git a/doc/refman/Classes.tex b/doc/refman/Classes.tex
index d6a553e1a8..58ae7191f8 100644
--- a/doc/refman/Classes.tex
+++ b/doc/refman/Classes.tex
@@ -392,11 +392,13 @@ than {\tt eauto} and {\tt auto}. The main differences are the following:
   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})
-  and will try to solve \emph{only} typeclass goals. Other subgoals are
-  automatically shelved and \emph{must be} resolved entirely when the
-  other typeclass subgoals are resolved or the proof search will fail
-  \emph{globally}, \emph{without} the possibility to find another
-  complete solution with no shelved subgoals.
+  and will try to solve \emph{only} typeclass goals. If some subgoal of
+  a hint/instance is non-dependent and not of class type, that hint
+  application will fail. Dependent subgoals are automatically shelved
+  and \emph{must be} resolved entirely when the other typeclass subgoals
+  are resolved or the proof search will fail \emph{globally},
+  \emph{without} the possibility to find another complete solution with
+  no shelved subgoals.
 
   \emph{Note: } As of Coq 8.6, {\tt all:once (typeclasses eauto)}
   faithfully mimicks what happens during typeclass resolution when it is
-- 
cgit v1.2.3


From 5939d426ac785ec063e66a302f3692b645993c56 Mon Sep 17 00:00:00 2001
From: Cyprien Mangin
Date: Wed, 28 Sep 2016 16:56:22 +0200
Subject: Add documentation for [Set Warnings] and the -w option.

---
 doc/refman/RefMan-com.tex |  6 ++++++
 doc/refman/RefMan-oth.tex | 13 +++++++++++++
 2 files changed, 19 insertions(+)

(limited to 'doc/refman')

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-oth.tex b/doc/refman/RefMan-oth.tex
index 919e7b5cdc..3a9db5ead2 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{all}|\nterm{none}|\nterm{w}$_1$,\ldots,%
+  \nterm{w}$_n$).]{{\tt Set Warnings (\nterm{all}|\nterm{none}|\nterm{w}$_1$,\ldots,%
+  \nterm{w}$_n$)}.\optindex{Warnings}}
+\label{SetWarnings}
+This command configures the display of warnings. It is experimental, and expects
+\texttt{all}, \texttt{none} or a comma-separated list of warning names or
+categories. Adding~\texttt{-} in front of a warning 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}}
-- 
cgit v1.2.3


From 29ff821da57e35d37b41be34febb275306c4809f Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Sat, 5 Nov 2016 11:33:42 +0100
Subject: Minor fix in documentation

---
 doc/refman/RefMan-tac.tex | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'doc/refman')

diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index 656ae57b95..54393e46f6 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -1278,7 +1278,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}
-- 
cgit v1.2.3


From d6edca2f025574fd84ef7e37a178c42674ff5840 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Sat, 5 Nov 2016 11:34:10 +0100
Subject: Credits for 8.6

---
 doc/refman/RefMan-pre.tex | 129 ++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 129 insertions(+)

(limited to 'doc/refman')

diff --git a/doc/refman/RefMan-pre.tex b/doc/refman/RefMan-pre.tex
index cb2ab5dc2f..c7a3c7415a 100644
--- a/doc/refman/RefMan-pre.tex
+++ b/doc/refman/RefMan-pre.tex
@@ -1087,6 +1087,135 @@ Paris, January 2015, revised December 2015,\\
 Hugo Herbelin, Matthieu Sozeau and the {\Coq} development team\\
 \end{flushright}
 
+\section*{Credits: version 8.6 (Stronger, Better, Faster Rooster)}
+
+{\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, state-of-the-art universe constraint checker that
+  can outperform the previous version by an order of magnitude, by
+  Jacques-Henri Jourdan.
+\item In CoqIDE and other asynchronous interfaces, more fine-grained
+  asynchronous processing and error reporting by Enrico Tassi.
+\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 Update of the beautifier by Hugo Herbelin, useful for switching
+  between versions.
+\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 and others.
+\item Irrefutable patterns in abstractions, by Daniel de Rauglaudre.
+\item Integration of {\tt ssreflect}'s subterm selection algorithm by
+  Enrico Tassi.
+\item Integration of {\tt LtacProf}, a profiler for {\tt Ltac} by Tobias
+  Tebbi, Jason Gross and Paul Steckler.
+\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.
+
+Many tactics have now more uniform behavior w.r.t. intro-patterns thanks
+to Hugo Herbelin who also improved the basic tactics here and there.
+
+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 were provided by Michael Soegtrop and Enrico Tassi
+(Windows), Maxime Dénès and Matthieu Sozeau (MacOS X). Packages are now
+regularly built on the continuous integration server.
+
+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.
+
+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
+Sherer and Beta Ziliani. It would however be impossible to mention with
+precision all the names of people 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 much more robust release than previous ones.
+
+General maintenance during part or whole of this period has been done by
+Pierre Boutillier, Pierre Courtieu, Maxime Dénès, Hugo Herbelin, Pierre
+Letouzey, Guillaume Melquiond, Pierre-Marie Pédrot, Matthieu Sozeau,
+Arnaud Spiwack, Enrico Tassi as well as Bruno Barras, Yves Bertot,
+Frédéric Besson, Assia Mahboubi, Yann Régis-Gianas. The development
+process was coordinated by Matthieu Sozeau with the help of Maxime
+Dénès, who was also in charge of the release process.
+
+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
 
-- 
cgit v1.2.3


From 25fc9919c6d86fa8119b1f0c8e5ddba156055c9d Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Sun, 6 Nov 2016 08:54:37 +0100
Subject: Fixes from Enrico's review

---
 doc/refman/RefMan-pre.tex | 29 +++++++++++++++--------------
 1 file changed, 15 insertions(+), 14 deletions(-)

(limited to 'doc/refman')

diff --git a/doc/refman/RefMan-pre.tex b/doc/refman/RefMan-pre.tex
index c7a3c7415a..669ba11e81 100644
--- a/doc/refman/RefMan-pre.tex
+++ b/doc/refman/RefMan-pre.tex
@@ -1113,8 +1113,8 @@ over 100 contributions integrated. The main user visible changes are:
 \item Irrefutable patterns in abstractions, by Daniel de Rauglaudre.
 \item Integration of {\tt ssreflect}'s subterm selection algorithm by
   Enrico Tassi.
-\item Integration of {\tt LtacProf}, a profiler for {\tt Ltac} by Tobias
-  Tebbi, Jason Gross and Paul Steckler.
+\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
@@ -1170,14 +1170,23 @@ 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 were provided by Michael Soegtrop and Enrico Tassi
-(Windows), Maxime Dénès and Matthieu Sozeau (MacOS X). Packages are now
-regularly built on the continuous integration server.
+Packaging tools and software development kits were prepared by Maxime
+Dénès, Michael Soegtrop 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.
 
 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.
 
+General maintenance during part or whole of this period has been done by
+Pierre Boutillier, Pierre Courtieu, Maxime Dénès, Hugo Herbelin, Pierre
+Letouzey, Guillaume Melquiond, Pierre-Marie Pédrot, Matthieu Sozeau,
+Arnaud Spiwack, Enrico Tassi, Bruno Barras, Yves Bertot,
+Frédéric Besson, Assia Mahboubi and Yann Régis-Gianas. The development
+process was coordinated by 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
@@ -1194,15 +1203,7 @@ development cycle. Its development spanned 10 months from the release of
 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 much more robust release than previous ones.
-
-General maintenance during part or whole of this period has been done by
-Pierre Boutillier, Pierre Courtieu, Maxime Dénès, Hugo Herbelin, Pierre
-Letouzey, Guillaume Melquiond, Pierre-Marie Pédrot, Matthieu Sozeau,
-Arnaud Spiwack, Enrico Tassi as well as Bruno Barras, Yves Bertot,
-Frédéric Besson, Assia Mahboubi, Yann Régis-Gianas. The development
-process was coordinated by Matthieu Sozeau with the help of Maxime
-Dénès, who was also in charge of the release process.
+in a hopefully much more robust release than previous ones.
 
 Coq Enhancement Proposals (CEPs for short) were introduced by Enrico
 Tassi to provide more visibility and a discussion period on new
-- 
cgit v1.2.3


From ceaafcde70e0ba536cae03baa740563aff47f6e8 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Sun, 6 Nov 2016 11:22:31 +0100
Subject: Maxime's comments

---
 doc/refman/RefMan-pre.tex | 36 ++++++++++++++++++++----------------
 1 file changed, 20 insertions(+), 16 deletions(-)

(limited to 'doc/refman')

diff --git a/doc/refman/RefMan-pre.tex b/doc/refman/RefMan-pre.tex
index 669ba11e81..944cd48481 100644
--- a/doc/refman/RefMan-pre.tex
+++ b/doc/refman/RefMan-pre.tex
@@ -1087,7 +1087,7 @@ Paris, January 2015, revised December 2015,\\
 Hugo Herbelin, Matthieu Sozeau and the {\Coq} development team\\
 \end{flushright}
 
-\section*{Credits: version 8.6 (Stronger, Better, Faster Rooster)}
+\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
@@ -1098,7 +1098,8 @@ over 100 contributions integrated. The main user visible changes are:
   can outperform the previous version by an order of magnitude, by
   Jacques-Henri Jourdan.
 \item In CoqIDE and other asynchronous interfaces, more fine-grained
-  asynchronous processing and error reporting by Enrico Tassi.
+  asynchronous processing and error reporting by Enrico Tassi (ability
+  to jump to any error in 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
@@ -1170,22 +1171,25 @@ 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 Maxime
-Dénès, Michael Soegtrop 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.
+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.
 
 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.
 
-General maintenance during part or whole of this period has been done by
-Pierre Boutillier, Pierre Courtieu, Maxime Dénès, Hugo Herbelin, Pierre
-Letouzey, Guillaume Melquiond, Pierre-Marie Pédrot, Matthieu Sozeau,
-Arnaud Spiwack, Enrico Tassi, Bruno Barras, Yves Bertot,
-Frédéric Besson, Assia Mahboubi and Yann Régis-Gianas. The development
-process was coordinated by Matthieu Sozeau with the help of Maxime
-Dénès, who was also in charge of the release process.
+The contributors for this version are C.J. Bell, Yves Bertot, Frédéric
+Besson, Tej Chajed, Pierre Courtieu, Maxime Dénès, Ricky Elrod, Jason
+Gross, Hugo Herbelin, Emilio Jesus Gallego Arias, Jacques-Henri Jourdan,
+Matej Košík, Xavier Leroy, Pierre Letouzey, Gregory Malecha, Cyprien
+Mangin, Erik Martin-Dorel, Guillaume Melquiond, Pierre-Marie Pédrot,
+Lionel Rieg, Gabriel Scherer, Matthieu Sozeau, Arnaud Spiwack, Paul
+Steckler, Laurent Théry, Enrico Tassi, Nickolai Zeldovich, Théo
+Zimmermann and Daniel de Rauglaudre. 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
@@ -1193,8 +1197,8 @@ 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
-Sherer and Beta Ziliani. It would however be impossible to mention with
-precision all the names of people who to some extent influenced the
+Sherer 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
@@ -1203,7 +1207,7 @@ development cycle. Its development spanned 10 months from the release of
 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 much more robust release than previous ones.
+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
-- 
cgit v1.2.3


From bf8827788d1d8c0dc96b963d3c35985d8b3725c6 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Sun, 6 Nov 2016 11:48:06 +0100
Subject: Hugo's comments

---
 doc/refman/RefMan-pre.tex | 2 --
 1 file changed, 2 deletions(-)

(limited to 'doc/refman')

diff --git a/doc/refman/RefMan-pre.tex b/doc/refman/RefMan-pre.tex
index 944cd48481..6ba2f850ee 100644
--- a/doc/refman/RefMan-pre.tex
+++ b/doc/refman/RefMan-pre.tex
@@ -1106,8 +1106,6 @@ over 100 contributions integrated. The main user visible changes are:
   Cyprien Mangin, Matthieu Sozeau and Arnaud Spiwack.
 \item Tactic behavior uniformization and specification, generalization
   of intro-patterns by Hugo Herbelin and others.
-\item Update of the beautifier by Hugo Herbelin, useful for switching
-  between versions.
 \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 and others.
-- 
cgit v1.2.3


From a96fed4624d8baaa4bec9bb63676eb1bcb389091 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Mon, 7 Nov 2016 09:36:30 +0100
Subject: Hugo and Maxime's 2nd pass of comments

---
 doc/refman/RefMan-pre.tex | 26 ++++++++++++--------------
 1 file changed, 12 insertions(+), 14 deletions(-)

(limited to 'doc/refman')

diff --git a/doc/refman/RefMan-pre.tex b/doc/refman/RefMan-pre.tex
index 6ba2f850ee..29ae51fea5 100644
--- a/doc/refman/RefMan-pre.tex
+++ b/doc/refman/RefMan-pre.tex
@@ -1108,7 +1108,7 @@ over 100 contributions integrated. The main user visible changes are:
   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 and others.
+  Melquiond, Pierre-Marie Pédrot and others.
 \item Irrefutable patterns in abstractions, by Daniel de Rauglaudre.
 \item Integration of {\tt ssreflect}'s subterm selection algorithm by
   Enrico Tassi.
@@ -1131,9 +1131,6 @@ tactics, and generalized and rationalized the handling of generic
 arguments, allowing to create new versions of Ltac more easily in the
 future.
 
-Many tactics have now more uniform behavior w.r.t. intro-patterns thanks
-to Hugo Herbelin who also improved the basic tactics here and there.
-
 In patterns and terms, {\tt @}, abbreviations and notations are now
 interpreted the same way, by Hugo Herbelin.
 
@@ -1179,15 +1176,16 @@ 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 C.J. Bell, Yves Bertot, Frédéric
-Besson, Tej Chajed, Pierre Courtieu, Maxime Dénès, Ricky Elrod, Jason
-Gross, Hugo Herbelin, Emilio Jesus Gallego Arias, Jacques-Henri Jourdan,
-Matej Košík, Xavier Leroy, Pierre Letouzey, Gregory Malecha, Cyprien
-Mangin, Erik Martin-Dorel, Guillaume Melquiond, Pierre-Marie Pédrot,
-Lionel Rieg, Gabriel Scherer, Matthieu Sozeau, Arnaud Spiwack, Paul
-Steckler, Laurent Théry, Enrico Tassi, Nickolai Zeldovich, Théo
-Zimmermann and Daniel de Rauglaudre. 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.
+Besson, Pierre Boutillier, Tej Chajed, Pierre Courtieu, Maxime Dénès,
+Ricky Elrod, Jason Gross, Hugo Herbelin, Sébastien Hinderer, Emilio
+Jesus Gallego Arias, Jacques-Henri Jourdan, Matej Košík, Xavier Leroy,
+Pierre Letouzey, Gregory Malecha, Cyprien Mangin, Erik Martin-Dorel,
+Guillaume Melquiond, Pierre-Marie Pédrot, Clément Pit-Claudel, Daniel de
+Rauglaudre, Lionel Rieg, Gabriel Scherer, Matthieu Sozeau, Arnaud
+Spiwack, Paul Steckler, Laurent Théry, Enrico Tassi, 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
@@ -1195,7 +1193,7 @@ 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
-Sherer and Beta Ziliani. It would however be impossible to mention
+Scherer and Beta Ziliani. It would however be impossible to mention
 exhaustively the names of everybody who to some extent influenced the
 development.
 
-- 
cgit v1.2.3


From 1692b9e8245fbf485c40c9b6dd311f124978e987 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Mon, 7 Nov 2016 13:49:57 +0100
Subject: More accurate contributor list.

Command used: git log v8.5..HEAD --pretty=format:"%an," | sort -k 2 | uniq

with some manual postprocessing for login names,  particles and multiple first names.
---
 doc/refman/RefMan-pre.tex | 23 ++++++++++++-----------
 1 file changed, 12 insertions(+), 11 deletions(-)

(limited to 'doc/refman')

diff --git a/doc/refman/RefMan-pre.tex b/doc/refman/RefMan-pre.tex
index 29ae51fea5..4578bee120 100644
--- a/doc/refman/RefMan-pre.tex
+++ b/doc/refman/RefMan-pre.tex
@@ -1175,24 +1175,25 @@ 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 C.J. Bell, Yves Bertot, Frédéric
-Besson, Pierre Boutillier, Tej Chajed, Pierre Courtieu, Maxime Dénès,
-Ricky Elrod, Jason Gross, Hugo Herbelin, Sébastien Hinderer, Emilio
-Jesus Gallego Arias, Jacques-Henri Jourdan, Matej Košík, Xavier Leroy,
+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 Jesus 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, Pierre-Marie Pédrot, Clément Pit-Claudel, Daniel de
-Rauglaudre, Lionel Rieg, Gabriel Scherer, Matthieu Sozeau, Arnaud
-Spiwack, Paul Steckler, Laurent Théry, Enrico Tassi, 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.
+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
+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.
-- 
cgit v1.2.3


From 25a60b1fcfa2f6017bedd986b1f90fe923d0f3ad Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Mon, 7 Nov 2016 14:50:56 +0100
Subject: Document two new variants of refine

They allow to call refine without doing typeclass resolution, allowing
to use refine in typeclass hints.
---
 doc/refman/RefMan-tac.tex | 10 ++++++++++
 1 file changed, 10 insertions(+)

(limited to 'doc/refman')

diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index 0aa179d627..695b0b883f 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}
-- 
cgit v1.2.3


From 3bc8d841148da0cf1db5b9b896f28c3285d4f5db Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Mon, 7 Nov 2016 17:31:48 +0100
Subject: After Emilio's comment.

---
 doc/refman/RefMan-pre.tex | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

(limited to 'doc/refman')

diff --git a/doc/refman/RefMan-pre.tex b/doc/refman/RefMan-pre.tex
index 4578bee120..8f75353bb3 100644
--- a/doc/refman/RefMan-pre.tex
+++ b/doc/refman/RefMan-pre.tex
@@ -1169,7 +1169,9 @@ 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.
+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
@@ -1178,7 +1180,7 @@ 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 Jesus Gallego Arias, Jason Gross, Hugo Herbelin,
+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
-- 
cgit v1.2.3


From cadb9e6614a1e72bf18f80acf0aabaeed4e9f057 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Tue, 8 Nov 2016 09:00:13 +0100
Subject: Rewording from Enrico

---
 doc/refman/RefMan-pre.tex | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

(limited to 'doc/refman')

diff --git a/doc/refman/RefMan-pre.tex b/doc/refman/RefMan-pre.tex
index 8f75353bb3..4f4f404422 100644
--- a/doc/refman/RefMan-pre.tex
+++ b/doc/refman/RefMan-pre.tex
@@ -1098,8 +1098,9 @@ over 100 contributions integrated. The main user visible changes are:
   can outperform the previous version by an order of magnitude, by
   Jacques-Henri Jourdan.
 \item In CoqIDE and other asynchronous interfaces, more fine-grained
-  asynchronous processing and error reporting by Enrico Tassi (ability
-  to jump to any error in the document).
+  asynchronous processing and error reporting by Enrico Tassi. In
+  asynchronous mode {\Coq} is now 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
-- 
cgit v1.2.3


From c60d155c2213461b8e4392b729445486086302d9 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Tue, 8 Nov 2016 09:36:42 +0100
Subject: Update documentation of Arguments after recent changes.

---
 doc/refman/RefMan-ext.tex | 12 ++++++------
 doc/refman/RefMan-syn.tex | 14 +++++++-------
 2 files changed, 13 insertions(+), 13 deletions(-)

(limited to 'doc/refman')

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-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.
-- 
cgit v1.2.3


From 034db0eae27c427a09092c337874c713474f50cb Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Wed, 9 Nov 2016 14:15:12 +0100
Subject: Update CHANGES and credits for 8.6beta1.

---
 doc/refman/RefMan-pre.tex | 13 ++++++-------
 1 file changed, 6 insertions(+), 7 deletions(-)

(limited to 'doc/refman')

diff --git a/doc/refman/RefMan-pre.tex b/doc/refman/RefMan-pre.tex
index 4f4f404422..f36969e821 100644
--- a/doc/refman/RefMan-pre.tex
+++ b/doc/refman/RefMan-pre.tex
@@ -1094,13 +1094,11 @@ Hugo Herbelin, Matthieu Sozeau and the {\Coq} development team\\
 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, state-of-the-art universe constraint checker that
-  can outperform the previous version by an order of magnitude, by
+\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. In
-  asynchronous mode {\Coq} is now capable of recovering from errors 
-  and continue processing the document.
+  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
@@ -1111,8 +1109,9 @@ over 100 contributions integrated. The main user visible changes are:
   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 Integration of {\tt ssreflect}'s subterm selection algorithm by
-  Enrico Tassi.
+\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}
-- 
cgit v1.2.3


From 30f222b1aad7ec483902b74dfa7dad7aefd5fca3 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Thu, 10 Nov 2016 13:24:28 +0100
Subject: Do not mention "none" in warnings doc, as it is there for
 compatibility.

---
 doc/refman/RefMan-oth.tex | 22 +++++++++++-----------
 1 file changed, 11 insertions(+), 11 deletions(-)

(limited to 'doc/refman')

diff --git a/doc/refman/RefMan-oth.tex b/doc/refman/RefMan-oth.tex
index 3a9db5ead2..56ce753cd6 100644
--- a/doc/refman/RefMan-oth.tex
+++ b/doc/refman/RefMan-oth.tex
@@ -914,18 +914,18 @@ 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{all}|\nterm{none}|\nterm{w}$_1$,\ldots,%
-  \nterm{w}$_n$).]{{\tt Set Warnings (\nterm{all}|\nterm{none}|\nterm{w}$_1$,\ldots,%
-  \nterm{w}$_n$)}.\optindex{Warnings}}
+\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
-\texttt{all}, \texttt{none} or a comma-separated list of warning names or
-categories. Adding~\texttt{-} in front of a warning 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}.
+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}
-- 
cgit v1.2.3


From 4b8f19c58a2b6cc841db2c011d23aa8106211fd6 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Tue, 15 Nov 2016 13:53:57 +0100
Subject: Revert part of a477dc, disallow_shelved

In only_classes mode we do not try to implement a stricter semantics for
shelved goals in 8.6. Leaving this for 8.7.
Update the documentation as well.
Remove a spurious printf call as well.

Fix test-suite now that shelved goals are allowed
---
 doc/refman/Classes.tex | 13 ++++++-------
 1 file changed, 6 insertions(+), 7 deletions(-)

(limited to 'doc/refman')

diff --git a/doc/refman/Classes.tex b/doc/refman/Classes.tex
index 58ae7191f8..7c4bd4d201 100644
--- a/doc/refman/Classes.tex
+++ b/doc/refman/Classes.tex
@@ -392,13 +392,12 @@ than {\tt eauto} and {\tt auto}. The main differences are the following:
   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})
-  and will try to solve \emph{only} typeclass goals. If some subgoal of
-  a hint/instance is non-dependent and not of class type, that hint
-  application will fail. Dependent subgoals are automatically shelved
-  and \emph{must be} resolved entirely when the other typeclass subgoals
-  are resolved or the proof search will fail \emph{globally},
-  \emph{without} the possibility to find another complete solution with
-  no shelved subgoals.
+  and will try to solve \emph{only} typeclass goals, shelving the other
+  goals. If some subgoal of a hint/instance is non-dependent and not of
+  class type, the hint application will fail when faced with that
+  subgoal. 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
-- 
cgit v1.2.3


From 09fd1e8b5e810bae0e50ecd4901cd7c8f1464f4a Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Wed, 16 Nov 2016 10:45:25 +0100
Subject: Revert more of a477dc for good measure

We stop failing automatically on non-declared-class nested or toplevel
subgoals as in 8.5, instead of the previous a477dc behavior of shelving
those goals and failing if shelved goals remained at the end of
resolution. It means typeclass resolution during refinement is closer to
all:typeclasses eauto. Hints in typeclass_instances for non-declared
classes can be used during resolution of _nested_ subgoals when it is
fired from type-inference, toplevel goals considered in this case are
still only classes (as in 8.5 and before). The code that triggers the
restriction to only declared class subgoals is commented.

Revert changes to test-suite, adding test for #5203, #5198 is fixed too.

Add corresponding tests in the test-suite (that will break if we,
e.g. disallow non-class subgoals) and update the refman accordingly.
---
 doc/refman/Classes.tex | 16 ++++++++--------
 1 file changed, 8 insertions(+), 8 deletions(-)

(limited to 'doc/refman')

diff --git a/doc/refman/Classes.tex b/doc/refman/Classes.tex
index 7c4bd4d201..bd8ee450ef 100644
--- a/doc/refman/Classes.tex
+++ b/doc/refman/Classes.tex
@@ -391,19 +391,19 @@ than {\tt eauto} and {\tt auto}. The main differences are the following:
   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})
-  and will try to solve \emph{only} typeclass goals, shelving the other
-  goals. If some subgoal of a hint/instance is non-dependent and not of
-  class type, the hint application will fail when faced with that
-  subgoal. Dependent subgoals are automatically shelved, and shelved
+  {\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. It might move to {\tt
-    all:typeclasses eauto} in future versions when the refinement engine
-  will be able to backtrack.
+  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.
-- 
cgit v1.2.3