Merge PR #12499: Clean future goals

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

1 files changed, 4 insertions, 10 deletions

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)