diff options
| author | Matthieu Sozeau | 2016-10-29 19:07:21 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2016-11-03 16:26:40 +0100 |
| commit | f6916774eea2ecc1262377cb14c2d494a0486358 (patch) | |
| tree | fde2d5865f5d5e1201de86692135d785b086a55b /tactics | |
| parent | d51c384e52003668bd97ca44da77a14c91e5cb14 (diff) | |
Do not shelve non-class subgoals but fail, it should
be the instance writer's responsibility to not generated non-dependent
non-class subgoals (otherwise we loose compatibility as shown in
e.g. MathClasses, which goes into loops because of unexpectedly
unconstrained goals). Reflect it in the doc.
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/class_tactics.ml | 9 |
1 files changed, 5 insertions, 4 deletions
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index 91eb388b3e..fe12b54a13 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -1020,16 +1020,17 @@ module Search = struct Evd.add sigma gl evi') sigma goals - let shelve_nonclass info = + let fail_if_nonclass info = Proofview.Goal.enter { enter = fun gl -> let gl = Proofview.Goal.assume gl in let sigma = Sigma.to_evar_map (Proofview.Goal.sigma gl) in if is_class_type sigma (Proofview.Goal.concl gl) then Proofview.tclUNIT () else (if !typeclasses_debug > 1 then - Feedback.msg_debug (pr_depth info.search_depth ++ str": shelving non-class subgoal " ++ + Feedback.msg_debug (pr_depth info.search_depth ++ + str": failure due to non-class subgoal " ++ pr_ev sigma (Proofview.Goal.goal gl)); - Proofview.shelve) } + Proofview.tclZERO NotApplicableEx) } (** The general hint application tactic. tac1 + tac2 .... The choice of OR or ORELSE is determined @@ -1159,7 +1160,7 @@ module Search = struct if path_matches derivs [] then aux e tl else let filter = - if info.search_only_classes then shelve_nonclass info + if info.search_only_classes then fail_if_nonclass info else Proofview.tclUNIT () in ortac |