From 9043add656177eeac1491a73d2f3ab92bec0013c Mon Sep 17 00:00:00 2001
From: Benjamin Barenblat <bbaren@debian.org>
Date: Sat, 29 Dec 2018 14:31:27 -0500
Subject: Imported Upstream version 8.8.2

---
 engine/proofview_monad.ml | 42 ++++++++++++++++++++++++++++--------------
 1 file changed, 28 insertions(+), 14 deletions(-)

(limited to 'engine/proofview_monad.ml')

diff --git a/engine/proofview_monad.ml b/engine/proofview_monad.ml
index 6f52b3ee..52bcabf9 100644
--- a/engine/proofview_monad.ml
+++ b/engine/proofview_monad.ml
@@ -1,9 +1,11 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
 (*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
 (** This file defines the datatypes used as internal states by the
@@ -62,7 +64,7 @@ end
 
 (** We typically label nodes of [Trace.tree] with messages to
     print. But we don't want to compute the result. *)
-type lazy_msg = unit -> Pp.std_ppcmds
+type lazy_msg = unit -> Pp.t
 let pr_lazy_msg msg = msg ()
 
 (** Info trace. *)
@@ -149,13 +151,25 @@ module Info = struct
     CList.map_append (collapse_tree n) f
 end
 
+module StateStore = Store.Make(struct end)
+
+(* let (set_state, get_state) = StateDyn.Easy.make_dyn "goal_state" *)
+
+type goal = Evar.t
+type goal_with_state = Evar.t * StateStore.t
+
+let drop_state = fst
+let get_state = snd
+let goal_with_state g s = (g, s)
+let with_empty_state g = (g, StateStore.empty)
+let map_goal_with_state f (g, s) = (f g, s)
 
 (** Type of proof views: current [evar_map] together with the list of
     focused goals. *)
 type proofview = {
   solution : Evd.evar_map;
-  comb : Evar.t list;
-  shelf : Evar.t list;
+  comb : goal_with_state list;
+  shelf : goal list;
 }
 
 (** {6 Instantiation of the logic monad} *)
@@ -169,7 +183,7 @@ module P = struct
   type e = bool
 
   (** Status (safe/unsafe) * shelved goals * given up *)
-  type w = bool * Evar.t list
+  type w = bool * goal list
 
   let wunit = true , []
   let wprod (b1, g1) (b2, g2) = b1 && b2 , g1@g2
@@ -209,9 +223,9 @@ module Solution : State with type t := Evd.evar_map = struct
   let modify f = Pv.modify (fun pv -> { pv with solution = f pv.solution })
 end
 
-module Comb : State with type t = Evar.t list = struct
+module Comb : State with type t = goal_with_state list = struct
     (* spiwack: I don't know why I cannot substitute ([:=]) [t] with a type expression. *)
-  type t = Evar.t list
+  type t = goal_with_state list
   let get = Logical.map (fun {comb} -> comb) Pv.get
   let set c = Pv.modify (fun pv -> { pv with comb = c })
   let modify f = Pv.modify (fun pv -> { pv with comb = f pv.comb })
@@ -227,17 +241,17 @@ module Status : Writer with type t := bool = struct
   let put s = Logical.put (s, [])
 end
 
-module Shelf : State with type t = Evar.t list = struct
+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 = Evar.t list
+  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 = Evar.t list = struct
+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 = Evar.t list
+  type t = goal list
   let put gs = Logical.put (true, gs)
 end
 
-- 
cgit v1.2.3