Merge PR #12499: Clean future goals

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

7 files changed, 227 insertions, 163 deletions

diff --git a/engine/evarutil.ml b/engine/evarutil.ml
index 01c4e5fd72..7beb7ff738 100644
--- a/engine/evarutil.ml
+++ b/engine/evarutil.ml
@@ -522,9 +522,7 @@ let restrict_evar evd evk filter ?src candidates =
      let evd, evk' = Evd.restrict evk filter ?candidates ?src evd in
      (* Mark new evar as future goal, removing previous one,
         circumventing Proofview.advance but making Proof.run_tactic catch these. *)
-     let future_goals = Evd.save_future_goals evd in
-     let future_goals = Evd.filter_future_goals (fun evk' -> not (Evar.equal evk evk')) future_goals in
-     let evd = Evd.restore_future_goals evd future_goals in
+     let evd = Evd.remove_future_goal evd evk in
      (Evd.declare_future_goal evk' evd, evk')
 
 let rec check_and_clear_in_constr env evdref err ids global c =
diff --git a/engine/evd.ml b/engine/evd.ml
index 92657c41a9..62a818ee6f 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -451,8 +451,6 @@ let key id (_, idtoev) =
 
 end
 
-type goal_kind = ToShelve | ToGiveUp
-
 type evar_flags =
   { obligation_evars : Evar.Set.t;
     restricted_evars : Evar.t Evar.Map.t;
@@ -466,6 +464,133 @@ type side_effects = {
   seff_roles : side_effect_role Cmap.t;
 }
 
+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
+                                   [e] will inherit
+                                   properties (now: the
+                                   name) of the evar which
+                                   will be instantiated with
+                                   a term containing [e]. *)
+  }
+
+  val map_filter : (Evar.t -> Evar.t option) -> t -> t
+  (** Applies a function on the future goals *)
+
+  val filter : (Evar.t -> bool) -> t -> t
+  (** Applies a filter on the future goals *)
+
+  type stack
+
+  val empty_stack : stack
+
+  val push : stack -> stack
+  val pop : stack -> t * stack
+
+  val add : shelve:bool -> 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
+
+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
+                                   [e] will inherit
+                                   properties (now: the
+                                   name) of the evar which
+                                   will be instantiated with
+                                   a term containing [e]. *)
+  }
+
+  type stack = t list
+
+  let set f = function
+  | [] -> anomaly Pp.(str"future_goals stack should not be empty")
+  | hd :: tl ->
+    f hd :: tl
+
+  let add ~shelve ~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 principal =
+        if principal then
+          match fgl.principal with
+          | Some _ -> CErrors.user_err Pp.(str "Only one main subgoal per instantiation.")
+          | None -> Some evk
+        else fgl.principal
+      in
+      { comb; shelf; principal }
+    in
+    set add stack
+
+  let remove e stack =
+    let remove fgl =
+      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 }
+    in
+    List.map remove stack
+
+  let empty = {
+    principal = None;
+    comb = [];
+    shelf = [];
+  }
+
+  let empty_stack = [empty]
+
+  let push stack = empty :: stack
+
+  let pop stack =
+    match stack with
+    | [] -> anomaly Pp.(str"future_goals stack should not be empty")
+    | hd :: tl ->
+      hd, tl
+
+  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
+
+  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 }
+
+  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
+
+end
+
+
 type evar_map = {
   (* Existential variables *)
   defn_evars : evar_info EvMap.t;
@@ -481,17 +606,9 @@ type evar_map = {
   evar_flags : evar_flags;
   (** Interactive proofs *)
   effects    : side_effects;
-  future_goals : Evar.t list; (** list of newly created evars, to be
-                                  eventually turned into goals if not solved.*)
-  principal_future_goal : Evar.t option; (** if [Some e], [e] must be
-                                             contained
-                                             [future_goals]. The evar
-                                             [e] will inherit
-                                             properties (now: the
-                                             name) of the evar which
-                                             will be instantiated with
-                                             a term containing [e]. *)
-  future_goals_status : goal_kind EvMap.t;
+  future_goals : FutureGoals.stack; (** list of newly created evars, to be
+                                        eventually turned into goals if not solved.*)
+  given_up : Evar.Set.t;
   extras : Store.t;
 }
 
@@ -590,14 +707,9 @@ let new_evar evd ?name ?typeclass_candidate evi =
 let remove d e =
   let undf_evars = EvMap.remove e d.undf_evars in
   let defn_evars = EvMap.remove e d.defn_evars in
-  let principal_future_goal = match d.principal_future_goal with
-  | None -> None
-  | Some e' -> if Evar.equal e e' then None else d.principal_future_goal
-  in
-  let future_goals = List.filter (fun e' -> not (Evar.equal e e')) d.future_goals in
-  let future_goals_status = EvMap.remove e d.future_goals_status in
+  let future_goals = FutureGoals.remove e d.future_goals in
   let evar_flags = remove_evar_flags e d.evar_flags in
-  { d with undf_evars; defn_evars; principal_future_goal; future_goals; future_goals_status;
+  { d with undf_evars; defn_evars; future_goals;
            evar_flags }
 
 let find d e =
@@ -723,9 +835,8 @@ let empty = {
   metas      = Metamap.empty;
   effects    = empty_side_effects;
   evar_names = EvNames.empty; (* id<->key for undefined evars *)
-  future_goals = [];
-  principal_future_goal = None;
-  future_goals_status = EvMap.empty;
+  future_goals = FutureGoals.empty_stack;
+  given_up = Evar.Set.empty;
   extras = Store.empty;
 }
 
@@ -735,6 +846,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
@@ -1059,72 +1172,35 @@ let drop_side_effects evd =
 let eval_side_effects evd = evd.effects
 
 (* Future goals *)
-let declare_future_goal ?tag evk evd =
-  { evd with future_goals = evk::evd.future_goals;
-             future_goals_status = Option.fold_right (EvMap.add evk) tag evd.future_goals_status }
-
-let declare_principal_goal ?tag evk evd =
-  match evd.principal_future_goal with
-  | None -> { evd with
-    future_goals = evk::evd.future_goals;
-    principal_future_goal=Some evk;
-    future_goals_status = Option.fold_right (EvMap.add evk) tag evd.future_goals_status;
-    }
-  | Some _ -> CErrors.user_err Pp.(str "Only one main subgoal per instantiation.")
-
-type future_goals = Evar.t list * Evar.t option * goal_kind EvMap.t
-
-let future_goals evd = evd.future_goals
-
-let principal_future_goal evd = evd.principal_future_goal
-
-let save_future_goals evd =
-  (evd.future_goals, evd.principal_future_goal, evd.future_goals_status)
-
-let reset_future_goals evd =
-  { evd with future_goals = [] ; principal_future_goal = None;
-             future_goals_status = EvMap.empty }
-
-let restore_future_goals evd (gls,pgl,map) =
-  { evd with future_goals = gls ; principal_future_goal = pgl;
-             future_goals_status = map }
-
-let fold_future_goals f sigma (gls,pgl,map) =
-  List.fold_left f sigma gls
-
-let map_filter_future_goals f (gls,pgl,map) =
-  (* Note: map is now a superset of filtered evs, but its size should
-    not be too big, so that's probably ok not to update it *)
-  (List.map_filter f gls,Option.bind pgl f,map)
-
-let filter_future_goals f (gls,pgl,map) =
-  (List.filter f gls,Option.bind pgl (fun a -> if f a then Some a else None),map)
-
-let dispatch_future_goals_gen distinguish_shelf (gls,pgl,map) =
-  let rec aux (comb,shelf,givenup as acc) = function
-    | [] -> acc
-    | evk :: gls ->
-       let acc =
-        try match EvMap.find evk map with
-        | ToGiveUp -> (comb,shelf,evk::givenup)
-        | ToShelve ->
-           if distinguish_shelf then (comb,evk::shelf,givenup)
-           else raise Not_found
-        with Not_found -> (evk::comb,shelf,givenup) in
-       aux acc gls in
-  (* Note: this reverses the order of initial list on purpose *)
-  let (comb,shelf,givenup) = aux ([],[],[]) gls in
-  (comb,shelf,givenup,pgl)
-
-let dispatch_future_goals =
-  dispatch_future_goals_gen true
-
-let extract_given_up_future_goals goals =
-  let (comb,_,givenup,_) = dispatch_future_goals_gen false goals in
-  (comb,givenup)
-
-let shelve_on_future_goals shelved (gls,pgl,map) =
-  (shelved @ gls, pgl, List.fold_right (fun evk -> EvMap.add evk ToShelve) shelved map)
+let declare_future_goal ?(shelve=false) evk evd =
+  let future_goals = FutureGoals.add ~shelve ~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
+  { evd with future_goals }
+
+let push_future_goals evd =
+  { evd with future_goals = FutureGoals.push evd.future_goals }
+
+let pop_future_goals evd =
+  let hd, future_goals = FutureGoals.pop evd.future_goals in
+  hd, { evd with future_goals }
+
+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 }
+
+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 *)
@@ -1142,8 +1218,7 @@ let set_metas evd metas = {
   effects = evd.effects;
   evar_names = evd.evar_names;
   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 d338b06e0e..db5265ca0a 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,59 +347,54 @@ val drop_side_effects : evar_map -> evar_map
 
 (** {5 Future goals} *)
 
-type goal_kind = ToShelve | ToGiveUp
-
-val declare_future_goal : ?tag:goal_kind -> Evar.t -> evar_map -> evar_map
+val declare_future_goal : ?shelve:bool -> Evar.t -> evar_map -> evar_map
 (** Adds an existential variable to the list of future goals. For
     internal uses only. *)
 
-val declare_principal_goal : ?tag:goal_kind -> Evar.t -> evar_map -> evar_map
+val declare_principal_goal : ?shelve:bool -> 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. *)
 
-val future_goals : evar_map -> Evar.t list
-(** Retrieves the list of future goals. Used by the [refine] primitive
-    of the tactic engine. *)
+module FutureGoals : sig
 
-val principal_future_goal : evar_map -> Evar.t option
-(** Retrieves the name of the principal existential variable if there
-    is one. Used by the [refine] primitive of the tactic engine. *)
+  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
+                                   [e] will inherit
+                                   properties (now: the
+                                   name) of the evar which
+                                   will be instantiated with
+                                   a term containing [e]. *)
+  }
 
-type future_goals
+  val map_filter : (Evar.t -> Evar.t option) -> t -> t
+  (** Applies a function on the future goals *)
 
-val save_future_goals : evar_map -> future_goals
-(** Retrieves the list of future goals including the principal future
-    goal. Used by the [refine] primitive of the tactic engine. *)
+  val filter : (Evar.t -> bool) -> t -> t
+  (** Applies a filter on the future goals *)
 
-val reset_future_goals : evar_map -> evar_map
-(** Clears the list of future goals (as well as the principal future
-    goal). Used by the [refine] primitive of the tactic engine. *)
+end
 
-val restore_future_goals : evar_map -> future_goals -> evar_map
-(** Sets the future goals (including the principal future goal) to a
-    previous value. Intended to be used after a local list of future
-    goals has been consumed. Used by the [refine] primitive of the
-    tactic engine. *)
+val push_future_goals : evar_map -> evar_map
 
-val fold_future_goals : (evar_map -> Evar.t -> evar_map) -> evar_map -> future_goals -> evar_map
-(** Fold future goals *)
+val pop_future_goals : evar_map -> FutureGoals.t * evar_map
 
-val map_filter_future_goals : (Evar.t -> Evar.t option) -> future_goals -> future_goals
-(** Applies a function on the future goals *)
+val fold_future_goals : (evar_map -> Evar.t -> evar_map) -> evar_map -> evar_map
 
-val filter_future_goals : (Evar.t -> bool) -> future_goals -> future_goals
-(** Applies a filter on the future goals *)
+(** Fold future goals *)
+
+val shelve_on_future_goals : Evar.t list -> evar_map -> evar_map
+(** Push goals on the shelve of future goals *)
 
-val dispatch_future_goals : future_goals -> Evar.t list * 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 remove_future_goal : evar_map -> Evar.t -> evar_map
 
-val extract_given_up_future_goals : future_goals -> Evar.t list * Evar.t list
-(** An ad hoc variant for Proof.proof; not for general use *)
+val give_up : Evar.t -> evar_map -> evar_map
 
-val shelve_on_future_goals : Evar.t list -> future_goals -> future_goals
-(** Push goals on the shelve of future goals *)
+val given_up : evar_map -> Evar.Set.t
 
 (** {5 Sort variables}
 
diff --git a/engine/proofview.ml b/engine/proofview.ml
index fd8512d73e..2fc5ade0d2 100644
--- a/engine/proofview.ml
+++ b/engine/proofview.ml
@@ -60,6 +60,10 @@ 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
@@ -74,9 +78,10 @@ let dependent_init =
     entry, { solution = sol; comb = with_empty_state gl :: comb; shelf = [] }
   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,8 +235,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
 
@@ -747,17 +751,16 @@ 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 } >>
+  Pv.set { pv with shelf = []; solution = Evd.push_future_goals solution } >>
   tac >>= fun ans ->
   Pv.get >>= fun npv ->
   let { shelf = gls; solution = sigma } = npv 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.shelf (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
   Pv.set npv >> tclUNIT (gls', ans)
@@ -833,14 +836,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,16 +1015,14 @@ 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 })
 
   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
diff --git a/engine/proofview.mli b/engine/proofview.mli
index 0f49d2f5d8..8853013a84 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,14 +470,11 @@ 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
 
   (** Clears the future goals store in the proof view. *)
-  val reset_future_goals : proofview -> proofview
+  val push_future_goals : proofview -> proofview
 
   (** Give the evars the status of a goal (changes their source location
       and makes them unresolvable for type classes. *)
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. *)