Merge PR #12499: Clean future goals

Ack-by: SkySkimmer
Ack-by: ejgallego
Reviewed-by: mattam82
Reviewed-by: ppedrot

1 files changed, 7 insertions, 8 deletions

diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index 2f55cc071f..ccb69cf845 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -715,8 +715,8 @@ module Search = struct
             shelve_goals shelved <*>
               (if List.is_empty goals then tclUNIT ()
                else
-                 let sigma' = make_unresolvables (fun x -> List.mem_f Evar.equal x goals) sigma in
-                 with_shelf (Unsafe.tclEVARS sigma' <*> Unsafe.tclNEWGOALS (CList.map Proofview.with_empty_state goals)) >>=
+                 let make_unresolvables = tclEVARMAP >>= fun sigma -> Unsafe.tclEVARS @@ make_unresolvables (fun x -> List.mem_f Evar.equal x goals) sigma in
+                 with_shelf (make_unresolvables <*> Unsafe.tclNEWGOALS (CList.map Proofview.with_empty_state goals)) >>=
                       fun s -> result s i (Some (Option.default 0 k + j)))
           end
         in with_shelf res >>= fun (sh, ()) ->
@@ -934,7 +934,7 @@ module Search = struct
        let tac = tac <*> Proofview.Unsafe.tclGETGOALS >>=
          fun stuck -> Proofview.shelve_goals (List.map Proofview_monad.drop_state stuck) in
        let evm = Evd.set_typeclass_evars evm Evar.Set.empty in
-       let fgoals = Evd.save_future_goals evm in
+       let evm = Evd.push_future_goals evm in
        let _, pv = Proofview.init evm [] in
        let pv = Proofview.unshelve goalsl pv in
        try
@@ -956,20 +956,19 @@ module Search = struct
                          (str "leaking evar " ++ int (Evar.repr ev) ++
                             spc () ++ pr_ev evm' ev);
                      acc && okev) evm' true);
-           let fgoals = Evd.shelve_on_future_goals shelved fgoals in
-           let evm' = Evd.restore_future_goals evm' fgoals in
+           let _, evm' = Evd.pop_future_goals evm' in
+           let evm' = Evd.shelve_on_future_goals shelved evm' in
            let nongoals' =
              Evar.Set.fold (fun ev acc -> match Evarutil.advance evm' ev with
                  | Some ev' -> Evar.Set.add ev acc
                  | None -> acc) (Evar.Set.union goals nongoals) (Evd.get_typeclass_evars evm')
            in
+           (* let evm' = { evm' with metas = evm.metas } *)
            let evm' = evars_reset_evd ~with_conv_pbs:true ~with_univs:false evm' evm in
            let evm' = Evd.set_typeclass_evars evm' nongoals' in
              Some evm'
         in
-        let (), pv', (unsafe, shelved, gaveup), _ = Proofview.apply ~name ~poly env tac pv in
-        if not (List.is_empty gaveup) then
-          CErrors.anomaly (Pp.str "run_on_evars not assumed to apply tactics generating given up goals.");
+        let (), pv', (unsafe, shelved), _ = Proofview.apply ~name ~poly env tac pv in
         if Proofview.finished pv' then finish pv' shelved
         else raise Not_found
        with Logic_monad.TacticFailure _ -> raise Not_found