diff options
author | 2016-10-29 19:07:21 +0200 | |
---|---|---|
committer | 2016-11-03 16:26:40 +0100 | |
commit | f6916774eea2ecc1262377cb14c2d494a0486358 (patch) | |
tree | fde2d5865f5d5e1201de86692135d785b086a55b /doc/refman | |
parent | d51c384e52003668bd97ca44da77a14c91e5cb14 (diff) |
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.
Diffstat (limited to 'doc/refman')
-rw-r--r-- | doc/refman/Classes.tex | 12 |
1 files changed, 7 insertions, 5 deletions
diff --git a/doc/refman/Classes.tex b/doc/refman/Classes.tex index d6a553e1a..58ae7191f 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 |