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