Unify the shelves

Before this patch, the proof engine had three notions of shelves:
- A local shelf in `proofview`
- A global shelf in `Proof.t`
- A future shelf in `evar_map`

This has lead to a lot of confusion and limitations or bugs, because
some components have only a partial view of the shelf: the pretyper can
see only the future shelf, tactics can see only the local and future
shelves. In particular, this refactoring is needed for #7825.

The solution we choose is to move shelf information to the evar map, as
a shelf stack (for nested `unshelve` tacticals).

Closes #8770.
Closes #6292.

Co-authored-by: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>

18 files changed, 162 insertions, 154 deletions

diff --git a/engine/evd.ml b/engine/evd.ml
index b20700143f..65df2643f2 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -468,7 +468,6 @@ module FutureGoals : sig
 
   type t = private {
     comb : Evar.t list;
-    shelf : Evar.t list;
     principal : Evar.t option; (** if [Some e], [e] must be
                                    contained in
                                    [comb]. The evar
@@ -492,20 +491,17 @@ module FutureGoals : sig
   val push : stack -> stack
   val pop : stack -> t * stack
 
-  val add : shelve:bool -> principal:bool -> Evar.t -> stack -> stack
+  val add : principal:bool -> Evar.t -> stack -> stack
   val remove : Evar.t -> stack -> stack
 
   val fold : ('a -> Evar.t -> 'a) -> 'a -> stack -> 'a
 
-  val put_shelf : Evar.t list -> stack -> stack
-
   val pr_stack : stack -> Pp.t
 
 end = struct
 
   type t = {
     comb : Evar.t list;
-    shelf : Evar.t list;
     principal : Evar.t option; (** if [Some e], [e] must be
                                    contained in
                                    [comb]. The evar
@@ -523,12 +519,9 @@ end = struct
   | hd :: tl ->
     f hd :: tl
 
-  let add ~shelve ~principal evk stack =
+  let add ~principal evk stack =
     let add fgl =
-      let (comb,shelf) =
-        if shelve then (fgl.comb,evk::fgl.shelf)
-        else (evk::fgl.comb,fgl.shelf)
-      in
+      let comb = evk :: fgl.comb in
       let principal =
         if principal then
           match fgl.principal with
@@ -536,7 +529,7 @@ end = struct
           | None -> Some evk
         else fgl.principal
       in
-      { comb; shelf; principal }
+      { comb; principal }
     in
     set add stack
 
@@ -545,15 +538,13 @@ end = struct
       let filter e' = not (Evar.equal e e') in
       let principal = Option.filter filter fgl.principal in
       let comb = List.filter filter fgl.comb in
-      let shelf = List.filter filter fgl.shelf in
-      { principal; comb; shelf }
+      { principal; comb }
     in
     List.map remove stack
 
   let empty = {
     principal = None;
     comb = [];
-    shelf = [];
   }
 
   let empty_stack = [empty]
@@ -568,27 +559,17 @@ end = struct
 
   let fold f acc stack =
     let future_goals = List.hd stack in
-    let future_goals = future_goals.comb @ future_goals.shelf in
-    List.fold_left f acc future_goals
+    List.fold_left f acc future_goals.comb
 
   let filter f fgl =
     let comb = List.filter f fgl.comb in
-    let shelf = List.filter f fgl.shelf in
     let principal = Option.filter f fgl.principal in
-    { comb; shelf; principal }
+    { comb; principal }
 
   let map_filter f fgl =
     let comb = List.map_filter f fgl.comb in
-    let shelf = List.map_filter f fgl.shelf in
     let principal = Option.bind fgl.principal f in
-    { comb; shelf; principal }
-
-  let put_shelf shelved stack =
-    match stack with
-    | [] -> anomaly Pp.(str"future_goals stack should not be empty")
-    | hd :: tl ->
-      let shelf = shelved @ hd.shelf in
-      { hd with shelf } :: tl
+    { comb; principal }
 
   let pr_stack stack =
     let open Pp in
@@ -601,7 +582,6 @@ end = struct
 
 end
 
-
 type evar_map = {
   (* Existential variables *)
   defn_evars : evar_info EvMap.t;
@@ -620,6 +600,7 @@ type evar_map = {
   future_goals : FutureGoals.stack; (** list of newly created evars, to be
                                         eventually turned into goals if not solved.*)
   given_up : Evar.Set.t;
+  shelf : Evar.t list list;
   extras : Store.t;
 }
 
@@ -848,6 +829,7 @@ let empty = {
   evar_names = EvNames.empty; (* id<->key for undefined evars *)
   future_goals = FutureGoals.empty_stack;
   given_up = Evar.Set.empty;
+  shelf = [[]];
   extras = Store.empty;
 }
 
@@ -859,6 +841,8 @@ 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 has_shelved evd = not (List.for_all List.is_empty evd.shelf)
+
 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
@@ -1183,12 +1167,12 @@ let drop_side_effects evd =
 let eval_side_effects evd = evd.effects
 
 (* Future goals *)
-let declare_future_goal ?(shelve=false) evk evd =
-  let future_goals = FutureGoals.add ~shelve ~principal:false evk evd.future_goals in
+let declare_future_goal evk evd =
+  let future_goals = FutureGoals.add ~principal:false evk evd.future_goals in
   { evd with future_goals }
 
-let declare_principal_goal ?(shelve=false) evk evd =
-  let future_goals = FutureGoals.add ~shelve ~principal:true evk evd.future_goals in
+let declare_principal_goal evk evd =
+  let future_goals = FutureGoals.add ~principal:true evk evd.future_goals in
   { evd with future_goals }
 
 let push_future_goals evd =
@@ -1201,10 +1185,6 @@ let pop_future_goals evd =
 let fold_future_goals f sigma =
   FutureGoals.fold f sigma sigma.future_goals
 
-let shelve_on_future_goals shelved evd =
-  let future_goals = FutureGoals.put_shelf shelved evd.future_goals in
-  { evd with future_goals }
-
 let remove_future_goal evd evk =
   { evd with future_goals = FutureGoals.remove evk evd.future_goals }
 
@@ -1214,8 +1194,36 @@ let pr_future_goals_stack evd =
 let give_up ev evd =
   { evd with given_up = Evar.Set.add ev evd.given_up }
 
+let push_shelf evd =
+  { evd with shelf = [] :: evd.shelf }
+
+let pop_shelf evd =
+  match evd.shelf with
+  | [] -> anomaly Pp.(str"shelf stack should not be empty")
+  | hd :: tl ->
+    hd, { evd with shelf = tl }
+
+let filter_shelf f evd =
+  { evd with shelf = List.map (List.filter f) evd.shelf }
+
+let shelve evd l =
+  match evd.shelf with
+  | [] -> anomaly Pp.(str"shelf stack should not be empty")
+  | hd :: tl ->
+    { evd with shelf = (hd@l) :: tl }
+
+let unshelve evd l =
+  { evd with shelf = List.map (List.filter (fun ev -> not (CList.mem_f Evar.equal ev l))) evd.shelf }
+
 let given_up evd = evd.given_up
 
+let shelf evd = List.flatten evd.shelf
+
+let pr_shelf evd =
+  let open Pp in
+  if List.is_empty evd.shelf then str"(empty stack)"
+  else prlist_with_sep (fun () -> str"||") (prlist_with_sep spc Evar.print) evd.shelf
+
 (**********************************************************)
 (* Accessing metas *)
 
@@ -1233,6 +1241,7 @@ let set_metas evd metas = {
   evar_names = evd.evar_names;
   future_goals = evd.future_goals;
   given_up = evd.given_up;
+  shelf = evd.shelf;
   extras = evd.extras;
 }
 
diff --git a/engine/evd.mli b/engine/evd.mli
index 9dc106a3d7..9394f9a9dd 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -171,6 +171,10 @@ 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 has_shelved : evar_map -> bool
+(** [has_shelved sigma] is [true] if and only if
+    there are shelved 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. *)
@@ -347,11 +351,11 @@ val drop_side_effects : evar_map -> evar_map
 
 (** {5 Future goals} *)
 
-val declare_future_goal : ?shelve:bool -> Evar.t -> evar_map -> evar_map
+val declare_future_goal : Evar.t -> evar_map -> evar_map
 (** Adds an existential variable to the list of future goals. For
     internal uses only. *)
 
-val declare_principal_goal : ?shelve:bool -> Evar.t -> evar_map -> evar_map
+val declare_principal_goal : Evar.t -> evar_map -> evar_map
 (** Adds an existential variable to the list of future goals and make
     it principal. Only one existential variable can be made principal, an
     error is raised otherwise. For internal uses only. *)
@@ -360,7 +364,6 @@ module FutureGoals : sig
 
   type t = private {
     comb : Evar.t list;
-    shelf : Evar.t list;
     principal : Evar.t option; (** if [Some e], [e] must be
                                    contained in
                                    [future_comb]. The evar
@@ -385,19 +388,29 @@ val pop_future_goals : evar_map -> FutureGoals.t * evar_map
 
 val fold_future_goals : (evar_map -> Evar.t -> evar_map) -> evar_map -> evar_map
 
-(** Fold future goals *)
-
-val shelve_on_future_goals : Evar.t list -> evar_map -> evar_map
-(** Push goals on the shelve of future goals *)
 
 val remove_future_goal : evar_map -> Evar.t -> evar_map
 
 val pr_future_goals_stack : evar_map -> Pp.t
 
+val push_shelf : evar_map -> evar_map
+
+val pop_shelf : evar_map -> Evar.t list * evar_map
+
+val filter_shelf : (Evar.t -> bool) -> evar_map -> evar_map
+
 val give_up : Evar.t -> evar_map -> evar_map
 
+val shelve : evar_map -> Evar.t list -> evar_map
+
+val unshelve : evar_map -> Evar.t list -> evar_map
+
 val given_up : evar_map -> Evar.Set.t
 
+val shelf : evar_map -> Evar.t list
+
+val pr_shelf : evar_map -> Pp.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 5b0e6f5785..978088872c 100644
--- a/engine/proofview.ml
+++ b/engine/proofview.ml
@@ -69,13 +69,13 @@ let dependent_init =
   let src = Loc.tag @@ Evar_kinds.GoalEvar in
   (* Main routine *)
   let rec aux = function
-  | TNil sigma -> [], { solution = sigma; comb = []; shelf = [] }
+  | TNil sigma -> [], { solution = sigma; comb = [] }
   | TCons (env, sigma, typ, t) ->
     let (sigma, econstr) = Evarutil.new_evar env sigma ~src ~typeclass_candidate:false typ in
     let (gl, _) = EConstr.destEvar sigma econstr in
     let ret, { solution = sol; comb = comb } = aux (t sigma econstr) in
     let entry = (econstr, typ) :: ret in
-    entry, { solution = sol; comb = with_empty_state gl :: comb; shelf = [] }
+    entry, { solution = sol; comb = with_empty_state gl :: comb }
   in
   fun t ->
     let t = map_telescope_evd Evd.push_future_goals t in
@@ -235,8 +235,6 @@ 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 = (status, state.shelf) in
-    let state = { state with shelf = [] } in
     r, state, status, Trace.to_tree info
 
 
@@ -621,7 +619,8 @@ let shelve =
   Comb.get >>= fun initial ->
   Comb.set [] >>
   InfoL.leaf (Info.Tactic (fun _ _ -> Pp.str"shelve")) >>
-  Shelf.modify (fun gls -> gls @ CList.map drop_state initial)
+  let initial = CList.map drop_state initial in
+  Pv.modify (fun pv -> { pv with solution = Evd.shelve pv.solution initial })
 
 let shelve_goals l =
   let open Proof in
@@ -629,7 +628,7 @@ let shelve_goals l =
   let comb = CList.filter (fun g -> not (CList.mem (drop_state g) l)) initial in
   Comb.set comb >>
   InfoL.leaf (Info.Tactic (fun _ _ -> Pp.str"shelve_goals")) >>
-  Shelf.modify (fun gls -> gls @ l)
+  Pv.modify (fun pv -> { pv with solution = Evd.shelve pv.solution l })
 
 (** [depends_on sigma src tgt] checks whether the goal [src] appears
     as an existential variable in the definition of the goal [tgt] in
@@ -696,7 +695,7 @@ let shelve_unifiable_informative =
   Comb.set n >>
   InfoL.leaf (Info.Tactic (fun _ _ -> Pp.str"shelve_unifiable")) >>
   let u = CList.map drop_state u in
-  Shelf.modify (fun gls -> gls @ u) >>
+  Pv.modify (fun pv -> { pv with solution = Evd.shelve pv.solution u }) >>
   tclUNIT u
 
 let shelve_unifiable =
@@ -716,13 +715,17 @@ let guard_no_unifiable =
       let l = CList.map (fun id -> Names.Name id) l in
       tclUNIT (Some l)
 
-(** [unshelve l p] adds all the goals in [l] at the end of the focused
-    goals of p *)
+(** [unshelve l p] moves all the goals in [l] from the shelf and put them at
+    the end of the focused goals of p, if they are still undefined after [advance] *)
 let unshelve l p =
+  let solution = Evd.unshelve p.solution l in
   let l = List.map with_empty_state l in
   (* advance the goals in case of clear *)
   let l = undefined p.solution l in
-  { p with comb = p.comb@l }
+  { comb = p.comb@l; solution }
+
+let filter_shelf f pv =
+  { pv with solution = Evd.filter_shelf f pv.solution }
 
 let mark_in_evm ~goal evd evars =
   let evd =
@@ -750,19 +753,20 @@ let mark_in_evm ~goal evd evars =
 let with_shelf tac =
   let open Proof in
   Pv.get >>= fun pv ->
-  let { shelf; solution } = pv in
-  Pv.set { pv with shelf = []; solution = Evd.push_future_goals solution } >>
+  let { solution } = pv in
+  Pv.set { pv with solution = Evd.push_shelf @@ Evd.push_future_goals solution } >>
   tac >>= fun ans ->
   Pv.get >>= fun npv ->
-  let { shelf = gls; solution = sigma } = npv in
+  let { solution = sigma } = npv in
+  let gls, sigma = Evd.pop_shelf sigma in
   (* The pending future goals are necessarily coming from V82.tactic *)
   (* and thus considered as to shelve, as in Proof.run_tactic *)
   let fgl, sigma = Evd.pop_future_goals sigma in
   (* Ensure we mark and return only unsolved goals *)
-  let gls' = CList.rev_append fgl.Evd.FutureGoals.shelf (CList.rev_append fgl.Evd.FutureGoals.comb gls) in
+  let gls' = CList.rev_append fgl.Evd.FutureGoals.comb gls in
   let gls' = undefined_evars sigma gls' in
   let sigma = mark_in_evm ~goal:false sigma gls' in
-  let npv = { npv with shelf; solution = sigma } in
+  let npv = { npv with solution = sigma } in
   Pv.set npv >> tclUNIT (gls', ans)
 
 (** [goodmod p m] computes the representative of [p] modulo [m] in the
@@ -993,6 +997,8 @@ let tclProofInfo =
 
 module Unsafe = struct
 
+  let (>>=) = tclBIND
+
   let tclEVARS evd =
     Pv.modify (fun ps -> { ps with solution = evd })
 
@@ -1002,21 +1008,22 @@ module Unsafe = struct
       { step with comb = step.comb @ gls }
     end
 
+  let tclNEWSHELVED gls =
+    Pv.modify begin fun step ->
+      let gls = undefined_evars step.solution gls in
+      { step with solution = Evd.shelve step.solution gls }
+    end
+
+  let tclGETSHELF = tclEVARMAP >>= fun sigma -> tclUNIT @@ Evd.shelf sigma
+
   let tclSETENV = Env.set
 
   let tclGETGOALS = Comb.get
 
   let tclSETGOALS = Comb.set
 
-  let tclGETSHELF = Shelf.get
-
-  let tclSETSHELF = Shelf.set
-
-  let tclPUTSHELF to_shelve =
-    tclBIND tclGETSHELF (fun shelf -> tclSETSHELF (to_shelve@shelf))
-
   let tclEVARSADVANCE evd =
-    Pv.modify (fun ps -> { ps with solution = evd; comb = undefined evd ps.comb })
+    Pv.modify (fun ps -> { solution = evd; comb = undefined evd ps.comb })
 
   let tclEVARUNIVCONTEXT ctx =
     Pv.modify (fun ps -> { ps with solution = Evd.set_universe_context ps.solution ctx })
@@ -1226,7 +1233,7 @@ module V82 = struct
       let sgs = CList.flatten goalss in
       let sgs = undefined evd sgs in
       InfoL.leaf (Info.Tactic (fun _ _ -> Pp.str"<unknown>")) >>
-      Pv.set { ps with solution = evd; comb = sgs; }
+      Pv.set { solution = evd; comb = sgs; }
     with e when catchable_exception e ->
       let (e, info) = Exninfo.capture e in
       tclZERO ~info e
@@ -1266,7 +1273,7 @@ module V82 = struct
   let of_tactic t gls =
     try
       let env = Global.env () in
-      let init = { shelf = []; solution = gls.Evd.sigma ; comb = [with_empty_state gls.Evd.it] } in
+      let init = { solution = gls.Evd.sigma ; comb = [with_empty_state gls.Evd.it] } in
       let name, poly = Names.Id.of_string "legacy_pe", false in
       let (_,final,_,_) = apply ~name ~poly (goal_env env gls.Evd.sigma gls.Evd.it) t init in
       { Evd.sigma = final.solution ; it = CList.map drop_state final.comb }
diff --git a/engine/proofview.mli b/engine/proofview.mli
index db6509c84e..816b45984b 100644
--- a/engine/proofview.mli
+++ b/engine/proofview.mli
@@ -162,7 +162,7 @@ val apply
   -> 'a tactic
   -> proofview
   -> 'a * proofview
-       * (bool*Evar.t list)
+       * bool
        * Proofview_monad.Info.tree
 
 (** {7 Monadic primitives} *)
@@ -331,17 +331,16 @@ val unifiable : Evd.evar_map -> Evar.t -> Evar.t list -> bool
     considered). *)
 val shelve_unifiable : unit tactic
 
-(** Idem but also returns the list of shelved variables *)
-val shelve_unifiable_informative : Evar.t list tactic
-
 (** [guard_no_unifiable] returns the list of unifiable goals if some
     goals are unifiable (see {!shelve_unifiable}) in the current focus. *)
 val guard_no_unifiable : Names.Name.t list option tactic
 
-(** [unshelve l p] adds all the goals in [l] at the end of the focused
-    goals of p *)
+(** [unshelve l p] moves all the goals in [l] from the shelf and put them at
+    the end of the focused goals of p, if they are still undefined after [advance] *)
 val unshelve : Evar.t list -> proofview -> proofview
 
+val filter_shelf : (Evar.t -> bool) -> proofview -> proofview
+
 (** [depends_on g1 g2 sigma] checks if g1 occurs in the type/ctx of g2 *)
 val depends_on : Evd.evar_map -> Evar.t -> Evar.t -> bool
 
@@ -454,6 +453,10 @@ module Unsafe : sig
       goal is already solved, it is not added. *)
   val tclNEWGOALS : Proofview_monad.goal_with_state list -> unit tactic
 
+  (** [tclNEWSHELVED gls] adds the goals [gls] to the shelf. If a
+      goal is already solved, it is not added. *)
+  val tclNEWSHELVED : Evar.t list -> unit tactic
+
   (** [tclSETGOALS gls] sets goals [gls] as the goals being under focus. If a
       goal is already solved, it is not set. *)
   val tclSETGOALS : Proofview_monad.goal_with_state list -> unit tactic
@@ -461,15 +464,9 @@ module Unsafe : sig
   (** [tclGETGOALS] returns the list of goals under focus. *)
   val tclGETGOALS : Proofview_monad.goal_with_state list tactic
 
-  (** [tclSETSHELF gls] sets goals [gls] as the current shelf. *)
-  val tclSETSHELF : Evar.t list -> unit tactic
-
   (** [tclGETSHELF] returns the list of goals on the shelf. *)
   val tclGETSHELF : Evar.t list tactic
 
-  (** [tclPUTSHELF] appends goals to the shelf. *)
-  val tclPUTSHELF : 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 4b3dd8f633..df9fc5dab3 100644
--- a/engine/proofview_monad.ml
+++ b/engine/proofview_monad.ml
@@ -166,7 +166,6 @@ let map_goal_with_state f (g, s) = (f g, s)
 type proofview = {
   solution : Evd.evar_map;
   comb : goal_with_state list;
-  shelf : goal list;
 }
 
 (** {6 Instantiation of the logic monad} *)
@@ -238,14 +237,6 @@ module Status : Writer with type t := bool = struct
   let put s = Logical.put s
 end
 
-module Shelf : State 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 get = Logical.map (fun {shelf} -> shelf) Pv.get
-  let set c = Pv.modify (fun pv -> { pv with shelf = c })
-  let modify f = Pv.modify (fun pv -> { pv with shelf = f pv.shelf })
-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 af866528c8..6cca3f5a5e 100644
--- a/engine/proofview_monad.mli
+++ b/engine/proofview_monad.mli
@@ -83,7 +83,6 @@ val map_goal_with_state : (goal -> goal) -> goal_with_state -> goal_with_state
 type proofview = {
   solution : Evd.evar_map;
   comb : goal_with_state list;
-  shelf : goal list;
 }
 
 (** {6 Instantiation of the logic monad} *)
@@ -137,10 +136,6 @@ module Env : State with type t := Environ.env
 (** Lens to the tactic status ([true] if safe, [false] if unsafe) *)
 module Status : Writer with type t := bool
 
-(** Lens to the list of goals which have been shelved during the
-    execution of the tactic. *)
-module Shelf : State 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/engine/termops.ml b/engine/termops.ml
index 7579631313..ac6870a39e 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -301,10 +301,12 @@ let pr_evar_map_gen with_univs pr_evars env sigma =
     if List.is_empty (Evd.meta_list sigma) then mt ()
     else
       str "METAS:" ++ brk (0, 1) ++ pr_meta_map env sigma
+  and shelf =
+    str "SHELF:" ++ brk (0, 1) ++ Evd.pr_shelf sigma ++ fnl ()
   and future_goals =
     str "FUTURE GOALS STACK:" ++ brk (0, 1) ++ Evd.pr_future_goals_stack sigma ++ fnl ()
   in
-  evs ++ svs ++ cstrs ++ typeclasses ++ obligations ++ metas ++ future_goals
+  evs ++ svs ++ cstrs ++ typeclasses ++ obligations ++ metas ++ shelf ++ future_goals
 
 let pr_evar_list env sigma l =
   let open Evd in
diff --git a/ide/coqide/idetop.ml b/ide/coqide/idetop.ml
index 751bddc7c4..ad21f663e4 100644
--- a/ide/coqide/idetop.ml
+++ b/ide/coqide/idetop.ml
@@ -220,11 +220,11 @@ 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 } process =
+let export_pre_goals Proof.{ sigma; goals; stack } 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.shelved_goals  = process @@ Evd.shelf sigma
   ; Interface.given_up_goals = process (Evar.Set.elements @@ Evd.given_up sigma)
   }
 
diff --git a/printing/printer.ml b/printing/printer.ml
index 0f635623e7..a1a2d9ae51 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -780,7 +780,8 @@ 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; sigma} = Proof.data p in
+  let Proof.{goals; stack; sigma} = Proof.data p in
+  let shelf = Evd.shelf sigma 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
diff --git a/proofs/proof.ml b/proofs/proof.ml
index 616cbf9678..d864aed25a 100644
--- a/proofs/proof.ml
+++ b/proofs/proof.ml
@@ -24,8 +24,6 @@
      the focus kind is actually stored inside the condition). To unfocus, one
      needs to know the focus kind, and the condition (for instance "no condition" or
      the proof under focused must be complete) must be met.
-   - Shelf: A list of goals which have been put aside during the proof. They can be
-     retrieved with the [Unshelve] command, or solved by side effects
    - Given up goals: as long as there is a given up goal, the proof is not completed.
      Given up goals cannot be retrieved, the user must go back where the tactic
      [give_up] was run and solve the goal there.
@@ -113,8 +111,6 @@ type t =
   (** History of the focusings, provides information on how to unfocus
      the proof and the extra information stored while focusing.  The
      list is empty when the proof is fully unfocused. *)
-  ; shelf : Goal.goal list
-  (** List of goals that have been shelved. *)
   ; name : Names.Id.t
   (** the name of the theorem whose proof is being constructed *)
   ; poly : bool
@@ -135,8 +131,7 @@ let proof p =
   let stack =
     map_minus_one (fun (_,_,c) -> Proofview.focus_context c) p.focus_stack
   in
-  let shelf = p.shelf in
-  (goals,stack,shelf,sigma)
+  (goals,stack,sigma)
 
 let rec unroll_focus pv = function
   | (_,_,ctx)::stk -> unroll_focus (Proofview.unfocus ctx pv) stk
@@ -152,7 +147,9 @@ let is_done p =
 (* spiwack: for compatibility with <= 8.2 proof engine *)
 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_shelved_goals p =
+  let (_goals,sigma) = Proofview.proofview p.proofview in
+  Evd.has_shelved sigma
 let has_given_up_goals p =
   let (_goals,sigma) = Proofview.proofview p.proofview in
   Evd.has_given_up sigma
@@ -216,13 +213,10 @@ let focus_id cond inf id pr =
         (* goal is already under focus *)
         _focus cond (Obj.repr inf) i i pr
      | None ->
-        if CList.mem_f Evar.equal ev pr.shelf then
+        if CList.mem_f Evar.equal ev (Evd.shelf evar_map) then
           (* goal is on the shelf, put it in focus *)
           let proofview = Proofview.unshelve [ev] pr.proofview in
-          let shelf =
-            CList.filter (fun ev' -> Evar.equal ev ev' |> not) pr.shelf
-          in
-          let pr = { pr with proofview; shelf } in
+          let pr = { pr with proofview } in
           let (focused_goals, _) = Proofview.proofview pr.proofview in
           let i =
             (* Now we know that this will succeed *)
@@ -290,7 +284,6 @@ let start ~name ~poly sigma goals =
     { proofview
     ; entry
     ; focus_stack = []
-    ; shelf = []
     ; name
     ; poly
   } in
@@ -302,7 +295,6 @@ let dependent_start ~name ~poly goals =
     { proofview
     ; entry
     ; focus_stack = []
-    ; shelf = []
     ; name
     ; poly
   } in
@@ -365,34 +357,41 @@ let run_tactic env tac pr =
   let open Proofview.Notations in
   let undef sigma l = List.filter (fun g -> Evd.is_undefined sigma g) l in
   let tac =
+    Proofview.tclEVARMAP >>= fun sigma ->
+    Proofview.Unsafe.tclEVARS (Evd.push_shelf sigma) >>= fun () ->
     tac >>= fun result ->
     Proofview.tclEVARMAP >>= fun sigma ->
     (* Already solved goals are not to be counted as shelved. Nor are
       they to be marked as unresolvable. *)
     let retrieved, sigma = Evd.pop_future_goals sigma in
     let retrieved = Evd.FutureGoals.filter (Evd.is_undefined sigma) retrieved in
-    let retrieved = List.rev_append retrieved.Evd.FutureGoals.shelf (List.rev retrieved.Evd.FutureGoals.comb) in
+    let retrieved = List.rev retrieved.Evd.FutureGoals.comb in
     let sigma = Proofview.Unsafe.mark_as_goals sigma retrieved in
+    let to_shelve, sigma = Evd.pop_shelf sigma in
     Proofview.Unsafe.tclEVARS sigma >>= fun () ->
-    Proofview.tclUNIT (result,retrieved)
+    Proofview.Unsafe.tclNEWSHELVED (retrieved@to_shelve) <*>
+    Proofview.tclUNIT (result,retrieved,to_shelve)
   in
   let { name; poly; proofview } = pr in
   let proofview = Proofview.Unsafe.push_future_goals proofview in
-  let ((result,retrieved),proofview,(status,to_shelve),info_trace) =
+  let ((result,retrieved,to_shelve),proofview,status,info_trace) =
     Proofview.apply ~name ~poly env tac proofview
   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
-  { pr with proofview ; shelf },(status,info_trace),result
+  let proofview = Proofview.filter_shelf (Evd.is_undefined sigma) proofview in
+  { pr with proofview },(status,info_trace),result
 
 (*** Commands ***)
 
 (* Remove all the goals from the shelf and adds them at the end of the
    focused goals. *)
 let unshelve p =
-  { p with proofview = Proofview.unshelve (p.shelf) (p.proofview) ; shelf = [] }
+  let sigma = Proofview.return p.proofview in
+  let shelf = Evd.shelf sigma in
+  let proofview = Proofview.unshelve shelf p.proofview in
+  { p with proofview }
 
 (*** Compatibility layer with <=v8.2 ***)
 module V82 = struct
@@ -438,22 +437,22 @@ module V82 = struct
     end in
     let { name; poly } = pr in
     let ((), proofview, _, _) = Proofview.apply ~name ~poly env tac pr.proofview in
-    let shelf =
-      List.filter begin fun g ->
+    let proofview = Proofview.filter_shelf
+      begin fun g ->
         Evd.is_undefined (Proofview.return proofview) g
-      end pr.shelf
+      end proofview
     in
-    { pr with proofview ; shelf }
+    { pr with proofview }
 
 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,sigma) = proof p in
+  let (goals,stack,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 (Evd.shelf sigma) 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
@@ -467,15 +466,13 @@ type data =
   (** Entry for the proofview *)
   ; stack : (Evar.t list * Evar.t list) list
   (** A representation of the focus stack *)
-  ; shelf : Evar.t list
-  (** A representation of the shelf  *)
   ; 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; name; poly } =
+let data { proofview; focus_stack; entry; 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. *)
@@ -486,10 +483,10 @@ let data { proofview; focus_stack; entry; shelf; name; poly } =
   in
   let stack =
     map_minus_one (fun (_,_,c) -> Proofview.focus_context c) focus_stack in
-  { sigma; goals; entry; stack; shelf; name; poly }
+  { sigma; goals; entry; stack; name; poly }
 
 let pr_proof p =
-  let { goals=fg_goals; stack=bg_goals; shelf; sigma } = data p in
+  let { goals=fg_goals; stack=bg_goals; sigma } = data p in
   Pp.(
     let pr_goal_list = prlist_with_sep spc Goal.pr_goal in
     let rec aux acc = function
@@ -499,7 +496,7 @@ let pr_proof p =
               pr_goal_list after) stack in
     str "[" ++ str "focus structure: " ++
                aux (pr_goal_list fg_goals) bg_goals ++ str ";" ++ spc () ++
-    str "shelved: " ++ pr_goal_list shelf ++ str ";" ++ spc () ++
+    str "shelved: " ++ pr_goal_list (Evd.shelf sigma) ++ str ";" ++ spc () ++
     str "given up: " ++ pr_goal_list (Evar.Set.elements @@ Evd.given_up sigma) ++
     str "]"
   )
@@ -580,7 +577,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; sigma; entry } = data prf in
+  let { goals; stack; sigma; entry } = data prf in
   assert (stack = []);
   let ans = match Proofview.initial_goals entry with
   | [c, _] -> c
@@ -597,9 +594,6 @@ let refine_by_tactic ~name ~poly env sigma ty tac =
   (* Push remaining goals as future_goals which is the only way we
      have to inform the caller that there are goals to collect while
      not being encapsulated in the monad *)
-  (* Goals produced by tactic "shelve" *)
-  let sigma = List.fold_right (Evd.declare_future_goal ~shelve:true) shelf 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
      itself. Note that this is unsound, because the tactic may have solved
diff --git a/proofs/proof.mli b/proofs/proof.mli
index ffb8380147..f487595dac 100644
--- a/proofs/proof.mli
+++ b/proofs/proof.mli
@@ -43,8 +43,6 @@ type data =
   (** Entry for the proofview *)
   ; stack : (Evar.t list * Evar.t list) list
   (** A representation of the focus stack *)
-  ; shelf : Evar.t list
-  (** A representation of the shelf  *)
   ; 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 51d6c923b6..dcff5e2b6c 100644
--- a/proofs/refine.ml
+++ b/proofs/refine.ml
@@ -92,7 +92,6 @@ let generic_refine ~typecheck f gl =
   in
   (* Mark goals *)
   let sigma = Proofview.Unsafe.mark_as_goals sigma future_goals.Evd.FutureGoals.comb in
-  let sigma = Proofview.Unsafe.mark_unresolvables sigma future_goals.Evd.FutureGoals.shelf in
   let comb = CList.rev_map (fun x -> Proofview.goal_with_state x state) future_goals.Evd.FutureGoals.comb in
   let trace env sigma = Pp.(hov 2 (str"simple refine"++spc()++
                                    Termops.Internal.print_constr_env env sigma c)) in
@@ -100,7 +99,6 @@ let generic_refine ~typecheck f gl =
   Proofview.Unsafe.tclSETENV (Environ.reset_context env) <*>
   Proofview.Unsafe.tclEVARS sigma <*>
   Proofview.Unsafe.tclSETGOALS comb <*>
-  Proofview.Unsafe.tclPUTSHELF @@ List.rev future_goals.Evd.FutureGoals.shelf <*>
   Proofview.tclUNIT v
   end
 
diff --git a/stm/proofBlockDelimiter.ml b/stm/proofBlockDelimiter.ml
index e41f62361d..f367167d48 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; 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
+        let Proof.{ goals=focused; stack=r1; sigma } = Proof.data proof in
+        let rest = List.(flatten (map (fun (x,y) -> x @ y) r1)) @ (Evd.shelf sigma) @ (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 ccb69cf845..d969dea19e 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -931,12 +931,14 @@ module Search = struct
            top_sort evm goals
          else Evar.Set.elements goals
        in
-       let tac = tac <*> Proofview.Unsafe.tclGETGOALS >>=
+       let goalsl = List.map Proofview_monad.with_empty_state goalsl in
+       let tac =
+         Proofview.Unsafe.tclNEWGOALS goalsl <*>
+         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 evm = Evd.push_future_goals evm in
        let _, pv = Proofview.init evm [] in
-       let pv = Proofview.unshelve goalsl pv in
        try
          (* Instance may try to call this before a proof is set up!
             Thus, give_me_the_proof will fail. Beware! *)
@@ -947,17 +949,17 @@ module Search = struct
             * with | Proof_global.NoCurrentProof -> *)
            Id.of_string "instance", false
          in
-         let finish pv' shelved =
+         let finish pv' =
            let evm' = Proofview.return pv' in
+           let shelf = Evd.shelf evm' in
              assert(Evd.fold_undefined (fun ev _ acc ->
-                     let okev = Evd.mem evm ev || List.mem ev shelved in
+                     let okev = Evd.mem evm ev || List.mem ev shelf in
                      if not okev then
                        Feedback.msg_debug
                          (str "leaking evar " ++ int (Evar.repr ev) ++
                             spc () ++ pr_ev evm' ev);
                      acc && okev) evm' true);
            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
@@ -968,8 +970,8 @@ module Search = struct
            let evm' = Evd.set_typeclass_evars evm' nongoals' in
              Some evm'
         in
-        let (), pv', (unsafe, shelved), _ = Proofview.apply ~name ~poly env tac pv in
-        if Proofview.finished pv' then finish pv' shelved
+        let (), pv', unsafe, _ = Proofview.apply ~name ~poly env tac pv in
+        if Proofview.finished pv' then finish pv'
         else raise Not_found
        with Logic_monad.TacticFailure _ -> raise Not_found
 
diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml
index 9917ae0f01..88924160ff 100644
--- a/toplevel/coqloop.ml
+++ b/toplevel/coqloop.ml
@@ -324,11 +324,11 @@ 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;sigma=sigma1} = Proof.data p1 in
-  let Proof.{goals=b1;stack=b2;shelf=b3;sigma=sigma2} = Proof.data p2 in
+  let Proof.{goals=a1;stack=a2;sigma=sigma1} = Proof.data p1 in
+  let Proof.{goals=b1;stack=b2;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 (Evd.shelf sigma1) (Evd.shelf sigma2) &&
   Evar.Set.equal (Evd.given_up sigma1) (Evd.given_up sigma2)
 
 let drop_last_doc = ref None
diff --git a/vernac/classes.ml b/vernac/classes.ml
index 82a1e32a14..02cb60f1cf 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -359,7 +359,7 @@ let declare_instance_open sigma ?hook ~tac ~global ~poly id pri impargs udecl id
      consequence, we use the low-level primitives to code
      the refinement manually.*)
   let future_goals, sigma = Evd.pop_future_goals sigma in
-  let gls = List.rev_append future_goals.Evd.FutureGoals.shelf (List.rev future_goals.Evd.FutureGoals.comb) in
+  let gls = List.rev future_goals.Evd.FutureGoals.comb in
   let sigma = Evd.push_future_goals sigma in
   let kind = Decls.(IsDefinition Instance) in
   let hook = Declare.Hook.(make (fun { S.dref ; _ } -> instance_hook pri global ?hook dref)) in
diff --git a/vernac/declare.ml b/vernac/declare.ml
index 12d6cb9f49..099a63cf8f 100644
--- a/vernac/declare.ml
+++ b/vernac/declare.ml
@@ -1553,11 +1553,11 @@ let set_used_variables ps l =
   ctx, { ps with section_vars = Some (Context.Named.to_vars ctx) }
 
 let get_open_goals ps =
-  let Proof.{ goals; stack; shelf } = Proof.data ps.proof in
+  let Proof.{ goals; stack; sigma } = Proof.data ps.proof in
   List.length goals +
   List.fold_left (+) 0
     (List.map (fun (l1,l2) -> List.length l1 + List.length l2) stack) +
-  List.length shelf
+  List.length (Evd.shelf sigma)
 
 type proof_object =
   { name : Names.Id.t
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 540e85621a..6a4c2a626d 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;sigma} = Proof.data proof in
+  let Proof.{goals; sigma} = Proof.data proof in
+  let shelf = Evd.shelf sigma in
   let given_up = Evar.Set.elements @@ Evd.given_up sigma in
   pr_evars_int sigma ~shelf ~given_up 1 (Evd.undefined_map sigma)