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