diff options
| author |  Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> | 2016-11-28 16:06:06 +0100 |
|---|---|---|
| committer | Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> | 2016-11-30 17:08:12 +0100 |
| commit | 910a1aec499b304006f2a9291811087ca3c4c7a1 (patch) | |
| tree | 5adf2914281774c841ffd63afdbd3b883e8bf66d /tactics | |
| parent | 823f0ab9c34f99d9171a5332a535c20d9f0f315c (diff) | |
Fix shelving order in typeclasses eauto.
Before this fix, unshelve typeclasses eauto would produce sub-goals
in the reverse order compared to when they were first shelved.
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 b47d8af56..b416bc657 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 |