1 files changed, 50 insertions, 38 deletions

diff --git a/engine/proofview.ml b/engine/proofview.ml
index fd8512d73e..978088872c 100644
--- a/engine/proofview.ml
+++ b/engine/proofview.ml
@@ -60,23 +60,28 @@ type telescope =
   | TNil of Evd.evar_map
   | TCons of Environ.env * Evd.evar_map * EConstr.types * (Evd.evar_map -> EConstr.constr -> telescope)
 
+let map_telescope_evd f = function
+  | TNil sigma -> TNil (f sigma)
+  | TCons (env,sigma,ty,g) -> TCons(env,(f sigma),ty,g)
+
 let dependent_init =
   (* Goals don't have a source location. *)
   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
     let entry, v = aux t in
     (* The created goal are not to be shelved. *)
-    let solution = Evd.reset_future_goals v.solution in
+    let _goals, solution = Evd.pop_future_goals v.solution in
     entry, { v with solution }
 
 let init =
@@ -230,9 +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, gaveup) = status in
-    let status = (status, state.shelf, gaveup) in
-    let state = { state with shelf = [] } in
     r, state, status, Trace.to_tree info
 
 
@@ -617,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
@@ -625,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
@@ -692,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 =
@@ -712,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 =
@@ -746,20 +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.reset_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 gls' = Evd.future_goals sigma in
-  let fgoals = Evd.save_future_goals solution in
-  let sigma = Evd.restore_future_goals sigma fgoals in
+  let fgl, sigma = Evd.pop_future_goals sigma in
   (* Ensure we mark and return only unsolved goals *)
-  let gls' = undefined_evars sigma (CList.rev_append gls' 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
@@ -833,14 +840,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} *)
@@ -986,6 +997,8 @@ let tclProofInfo =
 
 module Unsafe = struct
 
+  let (>>=) = tclBIND
+
   let tclEVARS evd =
     Pv.modify (fun ps -> { ps with solution = evd })
 
@@ -995,29 +1008,28 @@ 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 tclPUTGIVENUP = Giveup.put
-
   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 })
 
-  let reset_future_goals p =
-    { p with solution = Evd.reset_future_goals p.solution }
+  let push_future_goals p =
+    { p with solution = Evd.push_future_goals p.solution }
 
   let mark_as_goals evd content =
     mark_in_evm ~goal:true evd content
@@ -1032,8 +1044,8 @@ module Unsafe = struct
   let mark_as_unresolvables p evs =
     { p with solution = mark_in_evm ~goal:false p.solution evs }
 
-  let update_sigma_env pv env =
-    { pv with solution = Evd.update_sigma_env pv.solution env }
+  let update_sigma_univs ugraph pv =
+    { pv with solution = Evd.update_sigma_univs ugraph pv.solution }
 
 end
 
@@ -1221,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
@@ -1261,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 }