diff options
| -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 b47d8af56b..b416bc657a 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -1124,7 +1124,7 @@ module Search = struct else tclDISPATCH (List.init j (fun j' -> (tac_of gls i (Option.default 0 k + j)))) in - let finish sigma = + let finish nestedshelf sigma = let filter ev = try let evi = Evd.find_undefined sigma ev in @@ -1148,8 +1148,8 @@ module Search = struct (* Some existentials produced by the original tactic were not solved in the subgoals, turn them into subgoals now. *) let shelved, goals = List.partition (fun (ev, s) -> s) remaining in - let shelved = List.map fst shelved and goals = List.map fst goals in - if !typeclasses_debug > 1 && not (List.is_empty goals) then + let shelved = List.map fst shelved @ nestedshelf and goals = List.map fst goals in + if !typeclasses_debug > 1 && not (List.is_empty shelved && List.is_empty goals) then Feedback.msg_debug (str"Adding shelved subgoals to the search: " ++ prlist_with_sep spc (pr_ev sigma) goals ++ @@ -1162,7 +1162,8 @@ module Search = struct with_shelf (Unsafe.tclEVARS sigma' <*> Unsafe.tclNEWGOALS goals) >>= fun s -> result s i (Some (Option.default 0 k + j))) end - in res <*> tclEVARMAP >>= finish + in with_shelf res >>= fun (sh, ()) -> + tclEVARMAP >>= finish sh in if path_matches derivs [] then aux e tl else |