diff options
| author | Maxime Dénès | 2016-11-17 09:30:03 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2016-11-17 09:30:03 +0100 |
| commit | 63bb79ab8b488db728e46e5ada38d86d384acff1 (patch) | |
| tree | 6c9f70615b060d98cf371f460a4a5a3de5b44e27 /tactics | |
| parent | b072152fd5a1db47645981a2a0c542361da97420 (diff) | |
| parent | 37e0ce25f88a77c48c480e37ccca444a8f5fe4e8 (diff) | |
Merge remote-tracking branch 'github/pr/362' into v8.6
Was PR#362: Revert another part of a477dc in good measure
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/class_tactics.ml | 14 |
1 files changed, 7 insertions, 7 deletions
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index 99a1a98993..e44ace4257 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 @@ -1317,10 +1318,9 @@ module Search = struct Feedback.msg_debug (str"Starting resolution with " ++ int i ++ str" goal(s) under focus and " ++ int (List.length initshelf) ++ str " shelved goal(s)" ++ - if only_classes then str " in only_classes mode" else - str " in regular mode" ++ - match depth with None -> str ", unbounded" - | Some i -> str ", with depth limit " ++ int i)); + (if only_classes then str " in only_classes mode" else str " in regular mode") ++ + match depth with None -> str ", unbounded" + | Some i -> str ", with depth limit " ++ int i)); tac let run_on_evars p evm tac = |