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

1 files changed, 6 insertions, 7 deletions

diff --git a/doc/refman/Classes.tex b/doc/refman/Classes.tex
index 58ae7191f..7c4bd4d20 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