diff options
| author | Matthieu Sozeau | 2016-11-16 10:45:25 +0100 |
|---|---|---|
| committer | Matthieu Sozeau | 2016-11-16 16:24:01 +0100 |
| commit | 09fd1e8b5e810bae0e50ecd4901cd7c8f1464f4a (patch) | |
| tree | fae1680206dc022cd52374934376cb43926059d2 /tactics | |
| parent | 3a51aa7265f35dd3cbf3f7bff858d663e4406146 (diff) | |
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.
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/class_tactics.ml | 7 |
1 files changed, 4 insertions, 3 deletions
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 |