Move given_up goals to evar_map

16 files changed, 69 insertions, 85 deletions

diff --git a/engine/evd.ml b/engine/evd.ml
index fa84e45778..9de11bdc1e 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -451,7 +451,7 @@ let key id (_, idtoev) =
 
 end
 
-type goal_kind = ToShelve | ToGiveUp
+type goal_kind = ToShelve
 
 type evar_flags =
   { obligation_evars : Evar.Set.t;
@@ -492,6 +492,7 @@ type evar_map = {
                                              will be instantiated with
                                              a term containing [e]. *)
   future_goals_status : goal_kind EvMap.t;
+  given_up : Evar.Set.t;
   extras : Store.t;
 }
 
@@ -726,6 +727,7 @@ let empty = {
   future_goals = [];
   principal_future_goal = None;
   future_goals_status = EvMap.empty;
+  given_up = Evar.Set.empty;
   extras = Store.empty;
 }
 
@@ -735,6 +737,8 @@ let from_ctx ctx = { empty with universes = ctx }
 
 let has_undefined evd = not (EvMap.is_empty evd.undf_evars)
 
+let has_given_up evd = not (Evar.Set.is_empty evd.given_up)
+
 let evars_reset_evd ?(with_conv_pbs=false) ?(with_univs=true) evd d =
   let conv_pbs = if with_conv_pbs then evd.conv_pbs else d.conv_pbs in
   let last_mods = if with_conv_pbs then evd.last_mods else d.last_mods in
@@ -1105,33 +1109,33 @@ let filter_future_goals f evd =
   { evd with future_goals; principal_future_goal }
 
 let dispatch_future_goals_gen distinguish_shelf evd =
-  let rec aux (comb,shelf,givenup as acc) = function
+  let rec aux (comb,shelf as acc) = function
     | [] -> acc
     | evk :: gls ->
        let acc =
         try match EvMap.find evk evd.future_goals_status with
-        | ToGiveUp -> (comb,shelf,evk::givenup)
         | ToShelve ->
-           if distinguish_shelf then (comb,evk::shelf,givenup)
+           if distinguish_shelf then (comb,evk::shelf)
            else raise Not_found
-        with Not_found -> (evk::comb,shelf,givenup) in
+        with Not_found -> (evk::comb,shelf) in
        aux acc gls in
   (* Note: this reverses the order of initial list on purpose *)
-  let (comb,shelf,givenup) = aux ([],[],[]) evd.future_goals in
-  (comb,shelf,givenup,evd.principal_future_goal)
+  let (comb,shelf) = aux ([],[]) evd.future_goals in
+  (comb,shelf,evd.principal_future_goal)
 
 let dispatch_future_goals =
   dispatch_future_goals_gen true
 
-let extract_given_up_future_goals evd =
-  let (comb,_,givenup,_) = dispatch_future_goals_gen false evd in
-  (comb,givenup)
-
 let shelve_on_future_goals shelved evd =
   let future_goals = shelved @ evd.future_goals in
   let future_goals_status = List.fold_right (fun evk -> EvMap.add evk ToShelve) shelved evd.future_goals_status in
   {evd with future_goals; future_goals_status }
 
+let give_up ev evd =
+  { evd with given_up = Evar.Set.add ev evd.given_up }
+
+let given_up evd = evd.given_up
+
 (**********************************************************)
 (* Accessing metas *)
 
@@ -1150,6 +1154,7 @@ let set_metas evd metas = {
   future_goals = evd.future_goals;
   future_goals_status = evd.future_goals_status;
   principal_future_goal = evd.principal_future_goal;
+  given_up = evd.given_up;
   extras = evd.extras;
 }
 
diff --git a/engine/evd.mli b/engine/evd.mli
index 91cbbe5d77..4e3f95fc42 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -167,6 +167,10 @@ val has_undefined : evar_map -> bool
 (** [has_undefined sigma] is [true] if and only if
     there are uninstantiated evars in [sigma]. *)
 
+val has_given_up : evar_map -> bool
+(** [has_given_up sigma] is [true] if and only if
+    there are given up evars in [sigma]. *)
+
 val new_evar : evar_map ->
   ?name:Id.t -> ?typeclass_candidate:bool -> evar_info -> evar_map * Evar.t
 (** Creates a fresh evar mapping to the given information. *)
@@ -343,7 +347,7 @@ val drop_side_effects : evar_map -> evar_map
 
 (** {5 Future goals} *)
 
-type goal_kind = ToShelve | ToGiveUp
+type goal_kind = ToShelve
 
 val declare_future_goal : ?tag:goal_kind -> Evar.t -> evar_map -> evar_map
 (** Adds an existential variable to the list of future goals. For
@@ -387,16 +391,17 @@ val map_filter_future_goals : (Evar.t -> Evar.t option) -> evar_map -> evar_map
 val filter_future_goals : (Evar.t -> bool) -> evar_map -> evar_map
 (** Applies a filter on the future goals *)
 
-val dispatch_future_goals : evar_map -> Evar.t list * Evar.t list * Evar.t list * Evar.t option
+val dispatch_future_goals : evar_map -> Evar.t list * Evar.t list * Evar.t option
 (** Returns the future_goals dispatched into regular, shelved, given_up
    goals; last argument is the goal tagged as principal if any *)
 
-val extract_given_up_future_goals : evar_map -> Evar.t list * Evar.t list
-(** An ad hoc variant for Proof.proof; not for general use *)
-
 val shelve_on_future_goals : Evar.t list -> evar_map -> evar_map
 (** Push goals on the shelve of future goals *)
 
+val give_up : Evar.t -> evar_map -> evar_map
+
+val given_up : evar_map -> Evar.Set.t
+
 (** {5 Sort variables}
 
     Evar maps also keep track of the universe constraints defined at a given
diff --git a/engine/proofview.ml b/engine/proofview.ml
index fd8512d73e..0ed945f5d4 100644
--- a/engine/proofview.ml
+++ b/engine/proofview.ml
@@ -230,8 +230,7 @@ let apply ~name ~poly env t sp =
   match ans with
   | Nil (e, info) -> Exninfo.iraise (TacticFailure e, info)
   | Cons ((r, (state, _), status, info), _) ->
-    let (status, gaveup) = status in
-    let status = (status, state.shelf, gaveup) in
+    let status = (status, state.shelf) in
     let state = { state with shelf = [] } in
     r, state, status, Trace.to_tree info
 
@@ -833,14 +832,18 @@ let mark_as_unsafe = Status.put false
 
 (** Gives up on the goal under focus. Reports an unsafe status. Proofs
     with given up goals cannot be closed. *)
+
+let give_up evs pv =
+  let solution = List.fold_left (fun sigma ev -> Evd.give_up (drop_state ev) sigma) pv.solution evs in
+  { pv with solution }
+
 let give_up =
   let open Proof in
   Comb.get >>= fun initial ->
   Comb.set [] >>
   mark_as_unsafe >>
   InfoL.leaf (Info.Tactic (fun _ _ -> Pp.str"give_up")) >>
-  Giveup.put (CList.map drop_state initial)
-
+  Pv.modify (give_up initial)
 
 
 (** {7 Control primitives} *)
@@ -1008,8 +1011,6 @@ module Unsafe = struct
   let tclPUTSHELF to_shelve =
     tclBIND tclGETSHELF (fun shelf -> tclSETSHELF (to_shelve@shelf))
 
-  let tclPUTGIVENUP = Giveup.put
-
   let tclEVARSADVANCE evd =
     Pv.modify (fun ps -> { ps with solution = evd; comb = undefined evd ps.comb })
 
diff --git a/engine/proofview.mli b/engine/proofview.mli
index 0f49d2f5d8..29425b10f2 100644
--- a/engine/proofview.mli
+++ b/engine/proofview.mli
@@ -162,7 +162,7 @@ val apply
   -> 'a tactic
   -> proofview
   -> 'a * proofview
-       * (bool*Evar.t list*Evar.t list)
+       * (bool*Evar.t list)
        * Proofview_monad.Info.tree
 
 (** {7 Monadic primitives} *)
@@ -470,9 +470,6 @@ module Unsafe : sig
   (** [tclPUTSHELF] appends goals to the shelf. *)
   val tclPUTSHELF : Evar.t list -> unit tactic
 
-  (** [tclPUTGIVENUP] add an given up goal. *)
-  val tclPUTGIVENUP : Evar.t list -> unit tactic
-
   (** Sets the evar universe context. *)
   val tclEVARUNIVCONTEXT : UState.t -> unit tactic
 
diff --git a/engine/proofview_monad.ml b/engine/proofview_monad.ml
index 2f53d5bc73..4b3dd8f633 100644
--- a/engine/proofview_monad.ml
+++ b/engine/proofview_monad.ml
@@ -180,10 +180,10 @@ module P = struct
   type e = { trace: bool; name : Names.Id.t; poly : bool }
 
   (** Status (safe/unsafe) * shelved goals * given up *)
-  type w = bool * goal list
+  type w = bool
 
-  let wunit = true , []
-  let wprod (b1, g1) (b2, g2) = b1 && b2 , g1@g2
+  let wunit = true
+  let wprod b1 b2 = b1 && b2
 
   type u = Info.state
 
@@ -235,7 +235,7 @@ module Env : State with type t := Environ.env = struct
 end
 
 module Status : Writer with type t := bool = struct
-  let put s = Logical.put (s, [])
+  let put s = Logical.put s
 end
 
 module Shelf : State with type t = goal list = struct
@@ -246,12 +246,6 @@ module Shelf : State with type t = goal list = struct
   let modify f = Pv.modify (fun pv -> { pv with shelf = f pv.shelf })
 end
 
-module Giveup : Writer with type t = goal list = struct
-    (* spiwack: I don't know why I cannot substitute ([:=]) [t] with a type expression. *)
-  type t = goal list
-  let put gs = Logical.put (true, gs)
-end
-
 (** Lens and utilities pertaining to the info trace *)
 module InfoL = struct
   let recording = Logical.(map (fun {P.trace} -> trace) current)
diff --git a/engine/proofview_monad.mli b/engine/proofview_monad.mli
index a32b27904d..af866528c8 100644
--- a/engine/proofview_monad.mli
+++ b/engine/proofview_monad.mli
@@ -92,7 +92,7 @@ module P : sig
   type s = proofview * Environ.env
 
   (** Status (safe/unsafe) * given up *)
-  type w = bool * goal list
+  type w = bool
 
   val wunit : w
   val wprod : w -> w -> w
@@ -141,10 +141,6 @@ module Status : Writer with type t := bool
     execution of the tactic. *)
 module Shelf : State with type t = goal list
 
-(** Lens to the list of goals which were given up during the execution
-    of the tactic. *)
-module Giveup : Writer with type t = goal list
-
 (** Lens and utilities pertaining to the info trace *)
 module InfoL : sig
   (** [record_trace t] behaves like [t] and compute its [info] trace. *)
diff --git a/ide/coqide/idetop.ml b/ide/coqide/idetop.ml
index 2adc35ae3e..751bddc7c4 100644
--- a/ide/coqide/idetop.ml
+++ b/ide/coqide/idetop.ml
@@ -220,12 +220,12 @@ let process_goal_diffs diff_goal_map oldp nsigma ng =
   let (hyps_pp_list, concl_pp) = Proof_diffs.diff_goal_ide og_s ng nsigma in
   { Interface.goal_hyp = hyps_pp_list; Interface.goal_ccl = concl_pp; Interface.goal_id = Goal.uid ng }
 
-let export_pre_goals Proof.{ sigma; goals; stack; shelf; given_up } process =
+let export_pre_goals Proof.{ sigma; goals; stack; shelf } process =
   let process = List.map (process sigma) in
   { Interface.fg_goals       = process goals
   ; Interface.bg_goals       = List.(map (fun (lg,rg) -> process lg, process rg)) stack
   ; Interface.shelved_goals  = process shelf
-  ; Interface.given_up_goals = process given_up
+  ; Interface.given_up_goals = process (Evar.Set.elements @@ Evd.given_up sigma)
   }
 
 let goals () =
diff --git a/printing/printer.ml b/printing/printer.ml
index c5cb6ffad8..0f635623e7 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -780,17 +780,18 @@ let pr_open_subgoals_diff ?(quiet=false) ?(diffs=false) ?oproof proof =
      straightforward, but seriously, [Proof.proof] should return
      [evar_info]-s instead. *)
   let p = proof in
-  let Proof.{goals; stack; shelf; given_up; sigma} = Proof.data p in
+  let Proof.{goals; stack; shelf; sigma} = Proof.data p in
+  let given_up = Evd.given_up sigma in
   let stack = List.map (fun (l,r) -> List.length l + List.length r) stack in
   let seeds = Proof.V82.top_evars p in
   begin match goals with
   | [] -> let { Evd.it = bgoals ; sigma = bsigma } = Proof.V82.background_subgoals p in
           begin match bgoals,shelf,given_up with
-          | [] , [] , [] -> pr_subgoals None sigma ~seeds ~shelf ~stack ~unfocused:[] ~goals
+          | [] , [] , g when Evar.Set.is_empty g -> pr_subgoals None sigma ~seeds ~shelf ~stack ~unfocused:[] ~goals
           | [] , [] , _ ->
              Feedback.msg_info (str "No more subgoals, but there are some goals you gave up:");
              fnl ()
-            ++ pr_subgoals ~pr_first:false None bsigma ~seeds ~shelf:[] ~stack:[] ~unfocused:[] ~goals:given_up
+            ++ pr_subgoals ~pr_first:false None bsigma ~seeds ~shelf:[] ~stack:[] ~unfocused:[] ~goals:(Evar.Set.elements given_up)
             ++ fnl () ++ str "You need to go back and solve them."
           | [] , _ , _ ->
             Feedback.msg_info (str "All the remaining goals are on the shelf.");
diff --git a/proofs/goal.mli b/proofs/goal.mli
index a3aa1e248f..e8439120c0 100644
--- a/proofs/goal.mli
+++ b/proofs/goal.mli
@@ -65,4 +65,4 @@ module V82 : sig
 
 end
 
-module Set : sig include Set.S with type elt = goal end
+module Set = Evar.Set
diff --git a/proofs/proof.ml b/proofs/proof.ml
index c427c07b93..23998f8ba1 100644
--- a/proofs/proof.ml
+++ b/proofs/proof.ml
@@ -115,8 +115,6 @@ type t =
      list is empty when the proof is fully unfocused. *)
   ; shelf : Goal.goal list
   (** List of goals that have been shelved. *)
-  ; given_up : Goal.goal list
-  (** List of goals that have been given up *)
   ; name : Names.Id.t
   (** the name of the theorem whose proof is being constructed *)
   ; poly : bool
@@ -138,8 +136,7 @@ let proof p =
     map_minus_one (fun (_,_,c) -> Proofview.focus_context c) p.focus_stack
   in
   let shelf = p.shelf in
-  let given_up = p.given_up in
-  (goals,stack,shelf,given_up,sigma)
+  (goals,stack,shelf,sigma)
 
 let rec unroll_focus pv = function
   | (_,_,ctx)::stk -> unroll_focus (Proofview.unfocus ctx pv) stk
@@ -156,7 +153,9 @@ let is_done p =
 let has_unresolved_evar p =
   Proofview.V82.has_unresolved_evar p.proofview
 let has_shelved_goals p = not (CList.is_empty (p.shelf))
-let has_given_up_goals p = not (CList.is_empty (p.given_up))
+let has_given_up_goals p =
+  let (_goals,sigma) = Proofview.proofview p.proofview in
+  Evd.has_given_up sigma
 
 let is_complete p =
   is_done p && not (has_unresolved_evar p) &&
@@ -292,7 +291,6 @@ let start ~name ~poly sigma goals =
     ; entry
     ; focus_stack = []
     ; shelf = []
-    ; given_up = []
     ; name
     ; poly
   } in
@@ -305,7 +303,6 @@ let dependent_start ~name ~poly goals =
     ; entry
     ; focus_stack = []
     ; shelf = []
-    ; given_up = []
     ; name
     ; poly
   } in
@@ -374,25 +371,21 @@ let run_tactic env tac pr =
     (* Already solved goals are not to be counted as shelved. Nor are
       they to be marked as unresolvable. *)
     let retrieved = Evd.filter_future_goals (Evd.is_undefined sigma) sigma in
-    let retrieved,retrieved_given_up = Evd.extract_given_up_future_goals retrieved in
-    (* Check that retrieved given up is empty *)
-    if not (List.is_empty retrieved_given_up) then
-      CErrors.anomaly Pp.(str "Evars generated outside of proof engine (e.g. V82, clear, ...) are not supposed to be explicitly given up.");
+    let retrieved = List.rev @@ Evd.future_goals retrieved in
     let sigma = Proofview.Unsafe.mark_as_goals sigma retrieved in
     Proofview.Unsafe.tclEVARS sigma >>= fun () ->
     Proofview.tclUNIT (result,retrieved)
   in
   let { name; poly } = pr in
-  let ((result,retrieved),proofview,(status,to_shelve,give_up),info_trace) =
+  let ((result,retrieved),proofview,(status,to_shelve),info_trace) =
     Proofview.apply ~name ~poly env tac sp
   in
   let sigma = Proofview.return proofview in
   let to_shelve = undef sigma to_shelve in
   let shelf = (undef sigma pr.shelf)@retrieved@to_shelve in
   let proofview = Proofview.Unsafe.mark_as_unresolvables proofview to_shelve in
-  let given_up = pr.given_up@give_up in
   let proofview = Proofview.Unsafe.reset_future_goals proofview in
-  { pr with proofview ; shelf ; given_up },(status,info_trace),result
+  { pr with proofview ; shelf },(status,info_trace),result
 
 (*** Commands ***)
 
@@ -457,11 +450,11 @@ end
 let all_goals p =
   let add gs set =
     List.fold_left (fun s g -> Goal.Set.add g s) set gs in
-  let (goals,stack,shelf,given_up,_) = proof p in
+  let (goals,stack,shelf,sigma) = proof p in
     let set = add goals Goal.Set.empty in
     let set = List.fold_left (fun s gs -> let (g1, g2) = gs in add g1 (add g2 set)) set stack in
     let set = add shelf set in
-    let set = add given_up set in
+    let set = Goal.Set.union (Evd.given_up sigma) set in
     let { Evd.it = bgoals ; sigma = bsigma } = V82.background_subgoals p in
     add bgoals set
 
@@ -476,15 +469,13 @@ type data =
   (** A representation of the focus stack *)
   ; shelf : Evar.t list
   (** A representation of the shelf  *)
-  ; given_up : Evar.t list
-  (** A representation of the given up goals  *)
   ; name : Names.Id.t
   (** The name of the theorem whose proof is being constructed *)
   ; poly : bool
   (** Locality, polymorphism, and "kind" [Coercion, Definition, etc...] *)
   }
 
-let data { proofview; focus_stack; entry; shelf; given_up; name; poly } =
+let data { proofview; focus_stack; entry; shelf; name; poly } =
   let goals, sigma = Proofview.proofview proofview in
   (* spiwack: beware, the bottom of the stack is used by [Proof]
      internally, and should not be exposed. *)
@@ -495,10 +486,10 @@ let data { proofview; focus_stack; entry; shelf; given_up; name; poly } =
   in
   let stack =
     map_minus_one (fun (_,_,c) -> Proofview.focus_context c) focus_stack in
-  { sigma; goals; entry; stack; shelf; given_up; name; poly }
+  { sigma; goals; entry; stack; shelf; name; poly }
 
 let pr_proof p =
-  let { goals=fg_goals; stack=bg_goals; shelf; given_up; _ } = data p in
+  let { goals=fg_goals; stack=bg_goals; shelf; sigma } = data p in
   Pp.(
     let pr_goal_list = prlist_with_sep spc Goal.pr_goal in
     let rec aux acc = function
@@ -509,7 +500,7 @@ let pr_proof p =
     str "[" ++ str "focus structure: " ++
                aux (pr_goal_list fg_goals) bg_goals ++ str ";" ++ spc () ++
     str "shelved: " ++ pr_goal_list shelf ++ str ";" ++ spc () ++
-    str "given up: " ++ pr_goal_list given_up ++
+    str "given up: " ++ pr_goal_list (Evar.Set.elements @@ Evd.given_up sigma) ++
     str "]"
   )
 
@@ -589,7 +580,7 @@ let refine_by_tactic ~name ~poly env sigma ty tac =
       Exninfo.iraise (e, info)
   in
   (* Plug back the retrieved sigma *)
-  let { goals; stack; shelf; given_up; sigma; entry } = data prf in
+  let { goals; stack; shelf; sigma; entry } = data prf in
   assert (stack = []);
   let ans = match Proofview.initial_goals entry with
   | [c, _] -> c
@@ -608,8 +599,6 @@ let refine_by_tactic ~name ~poly env sigma ty tac =
      not being encapsulated in the monad *)
   (* Goals produced by tactic "shelve" *)
   let sigma = List.fold_right (Evd.declare_future_goal ~tag:Evd.ToShelve) shelf sigma in
-  (* Goals produced by tactic "give_up" *)
-  let sigma = List.fold_right (Evd.declare_future_goal ~tag:Evd.ToGiveUp) given_up sigma in
   (* Other goals *)
   let sigma = List.fold_right Evd.declare_future_goal goals sigma in
   (* Get rid of the fresh side-effects by internalizing them in the term
diff --git a/proofs/proof.mli b/proofs/proof.mli
index 2d4966676e..a0d4759bfc 100644
--- a/proofs/proof.mli
+++ b/proofs/proof.mli
@@ -45,8 +45,6 @@ type data =
   (** A representation of the focus stack *)
   ; shelf : Evar.t list
   (** A representation of the shelf  *)
-  ; given_up : Evar.t list
-  (** A representation of the given up goals  *)
   ; name : Names.Id.t
   (** The name of the theorem whose proof is being constructed *)
   ; poly : bool;
diff --git a/proofs/refine.ml b/proofs/refine.ml
index 8909b9639d..4244a9c900 100644
--- a/proofs/refine.ml
+++ b/proofs/refine.ml
@@ -75,7 +75,7 @@ let generic_refine ~typecheck f gl =
   let sigma = Evd.restore_future_goals sigma prev_future_goals in
   (* Select the goals *)
   let evs = Evd.map_filter_future_goals (Proofview.Unsafe.advance sigma) sigma' in
-  let comb,shelf,given_up,evkmain = Evd.dispatch_future_goals evs in
+  let comb,shelf,evkmain = Evd.dispatch_future_goals evs in
   (* Proceed to the refinement *)
   let sigma = match Proofview.Unsafe.advance sigma self with
   | None ->
@@ -102,7 +102,6 @@ let generic_refine ~typecheck f gl =
   Proofview.Unsafe.tclEVARS sigma <*>
   Proofview.Unsafe.tclSETGOALS comb <*>
   Proofview.Unsafe.tclPUTSHELF shelf <*>
-  Proofview.Unsafe.tclPUTGIVENUP given_up <*>
   Proofview.tclUNIT v
   end
 
diff --git a/stm/proofBlockDelimiter.ml b/stm/proofBlockDelimiter.ml
index 3d892fa5ca..e41f62361d 100644
--- a/stm/proofBlockDelimiter.ml
+++ b/stm/proofBlockDelimiter.ml
@@ -51,8 +51,8 @@ let is_focused_goal_simple ~doc id =
   | `Valid (Some { Vernacstate.lemmas }) ->
     Option.cata (Vernacstate.LemmaStack.with_top ~f:(fun proof ->
         let proof = Declare.Proof.get proof in
-        let Proof.{ goals=focused; stack=r1; shelf=r2; given_up=r3; sigma } = Proof.data proof in
-        let rest = List.(flatten (map (fun (x,y) -> x @ y) r1)) @ r2 @ r3 in
+        let Proof.{ goals=focused; stack=r1; shelf=r2; sigma } = Proof.data proof in
+        let rest = List.(flatten (map (fun (x,y) -> x @ y) r1)) @ r2 @ (Evar.Set.elements @@ Evd.given_up sigma) in
         if List.for_all (fun x -> simple_goal sigma x rest) focused
         then `Simple focused
         else `Not)) `Not lemmas
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index 31132824f5..597e60093b 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -967,9 +967,7 @@ module Search = struct
            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
diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml
index 79de3c86b6..9917ae0f01 100644
--- a/toplevel/coqloop.ml
+++ b/toplevel/coqloop.ml
@@ -324,12 +324,12 @@ let loop_flush_all () =
 let pequal cmp1 cmp2 (a1,a2) (b1,b2) = cmp1 a1 b1 && cmp2 a2 b2
 let evleq e1 e2 = CList.equal Evar.equal e1 e2
 let cproof p1 p2 =
-  let Proof.{goals=a1;stack=a2;shelf=a3;given_up=a4} = Proof.data p1 in
-  let Proof.{goals=b1;stack=b2;shelf=b3;given_up=b4} = Proof.data p2 in
+  let Proof.{goals=a1;stack=a2;shelf=a3;sigma=sigma1} = Proof.data p1 in
+  let Proof.{goals=b1;stack=b2;shelf=b3;sigma=sigma2} = Proof.data p2 in
   evleq a1 b1 &&
   CList.equal (pequal evleq evleq) a2 b2 &&
   CList.equal Evar.equal a3 b3 &&
-  CList.equal Evar.equal a4 b4
+  Evar.Set.equal (Evd.given_up sigma1) (Evd.given_up sigma2)
 
 let drop_last_doc = ref None
 
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 548f59559a..4e08a40d6b 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -112,7 +112,8 @@ let show_proof ~pstate =
 
 let show_top_evars ~proof =
   (* spiwack: new as of Feb. 2010: shows goal evars in addition to non-goal evars. *)
-  let Proof.{goals;shelf;given_up;sigma} = Proof.data proof in
+  let Proof.{goals;shelf;sigma} = Proof.data proof in
+  let given_up = Evar.Set.elements @@ Evd.given_up sigma in
   pr_evars_int sigma ~shelf ~given_up 1 (Evd.undefined_map sigma)
 
 let show_universes ~proof =