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.
---
 tactics/class_tactics.ml | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

(limited to 'tactics')

diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index 99a1a98993..4138562c64 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -1167,7 +1167,8 @@ module Search = struct
       if path_matches derivs [] then aux e tl
       else
         let filter =
-          if info.search_only_classes then fail_if_nonclass info
+          if false (* in 8.6, still allow non-class subgoals
+                    info.search_only_classes *) then fail_if_nonclass info
           else Proofview.tclUNIT ()
         in
         ortac
@@ -1238,8 +1239,8 @@ module Search = struct
         unit Proofview.tactic =
     let open Proofview in
     let open Proofview.Notations in
-    if only_classes && not (is_class_type sigma (Goal.concl gl)) then
-      Proofview.shelve
+    if false (* In 8.6, still allow non-class goals only_classes && not (is_class_type sigma (Goal.concl gl)) *) then
+      Tacticals.New.tclZEROMSG (str"Not a subgoal for a class")
     else
       let dep = dep || Proofview.unifiable sigma (Goal.goal gl) gls in
       let info = make_autogoal ?st only_classes dep (cut_of_hints hints) i gl in
-- 
cgit v1.2.3