1 files changed, 9 insertions, 19 deletions
diff --git a/engine/proofview_monad.ml b/engine/proofview_monad.ml
index 2f53d5bc73..80263694f5 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} *)
@@ -180,10 +179,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
 
@@ -203,6 +202,11 @@ module type State = sig
   val modify : (t->t) -> unit Logical.t
 end
 
+module type Reader = sig
+  type t
+  val get : t Logical.t
+end
+
 module type Writer = sig
   type t
   val put : t -> unit Logical.t
@@ -235,21 +239,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, [])
-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
-
-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)
+  let put s = Logical.put s
 end
 
 (** Lens and utilities pertaining to the info trace *)