diff options
| author | Matthieu Sozeau | 2016-03-21 17:31:05 +0100 |
|---|---|---|
| committer | Matthieu Sozeau | 2016-06-16 18:21:08 +0200 |
| commit | af9605c7d6929eb3c7699ba2824dd00bf06877db (patch) | |
| tree | b02cfa7605f088cac5d2c7aa95f650c9484dce80 /tactics | |
| parent | 37a8bf99b0f3c5adcbe27373e0d0b5622106ceee (diff) | |
Fix iterative deepening strategy failing too early
Report limit exceeded on _any_ branch so that we pursue search
if it was reached at least once. Add example by N. Tabareau in
test-suite.
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/class_tactics.ml | 17 |
1 files changed, 9 insertions, 8 deletions
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index 3c2ef406ee..fea8189eb6 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -555,6 +555,12 @@ let needs_backtrack' env evd unique concl = occur_existential concl else true +let merge_exceptions e e' = + match fst e, fst e' with + | ReachedLimitEx, _ -> e + | _, ReachedLimitEx -> e' + | _, _ -> e + let new_hints_tac_gl only_classes hints info kont gl : unit Proofview.tactic = @@ -615,7 +621,8 @@ let new_hints_tac_gl only_classes hints info kont gl else Proofview.tclDISPATCH (List.init j (tac_of i))) in if path_matches derivs [] then aux foundone e tl - else ortac (Proofview.tclBIND tac result) (fun e -> aux foundone e tl) + else ortac (Proofview.tclBIND tac result) + (fun e' -> aux foundone (merge_exceptions e e') tl) | [] -> if foundone == None && !typeclasses_debug then msg_debug (pr_depth info.search_depth ++ str": no match for " ++ @@ -624,7 +631,7 @@ let new_hints_tac_gl only_classes hints info kont gl str" possibilities"); match e with | (ReachedLimitEx,ie) -> Proofview.tclZERO ~info:ie ReachedLimitEx - | _ -> Tacticals.New.tclFAIL 0 (str"no hint applies") + | (_,ie) -> Proofview.tclZERO ~info:ie NotApplicableEx in aux None (NotApplicableEx,Exninfo.null) poss let new_hints_tac cl hints info kont : unit Proofview.tactic = @@ -659,12 +666,6 @@ let intro_tac' only_classes info kont = (fun _ -> Proofview.Goal.nf_enter { enter = fun gl -> intro_tac'' only_classes info kont gl }) -let merge_exceptions e e' = - match fst e, fst e' with - | ReachedLimitEx, _ -> e - | _, ReachedLimitEx -> e' - | _, _ -> e - let rec eauto_tac' only_classes hints limit depth = let kont info = Proofview.numgoals >>= fun i -> |