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.mli | 35 +++++++++++++++++++++++------------
 1 file changed, 23 insertions(+), 12 deletions(-)

(limited to 'engine/proofview_monad.mli')

diff --git a/engine/proofview_monad.mli b/engine/proofview_monad.mli
index 637414cc..9d752421 100644
--- a/engine/proofview_monad.mli
+++ b/engine/proofview_monad.mli
@@ -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
@@ -43,7 +45,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
 
 (** Info trace. *)
 module Info : sig
@@ -58,7 +60,7 @@ module Info : sig
   type state = tag Trace.incr
   type tree = tag Trace.forest
 
-  val print : tree -> Pp.std_ppcmds
+  val print : tree -> Pp.t
 
   (** [collapse n t] flattens the first [n] levels of [Tactic] in an
       info trace, effectively forgetting about the [n] top level of
@@ -67,12 +69,21 @@ module Info : sig
 
 end
 
+module StateStore : Store.S
+type goal = Evar.t
+type goal_with_state
+val drop_state : goal_with_state -> goal
+val get_state : goal_with_state -> StateStore.t
+val goal_with_state : goal -> StateStore.t -> goal_with_state
+val with_empty_state : goal -> goal_with_state
+val map_goal_with_state : (goal -> goal) -> goal_with_state -> goal_with_state
+
 (** 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} *)
@@ -81,7 +92,7 @@ module P : sig
   type s = proofview * Environ.env
 
   (** Status (safe/unsafe) * given up *)
-  type w = bool * Evar.t list
+  type w = bool * goal list
 
   val wunit : w
   val wprod : w -> w -> w
@@ -118,7 +129,7 @@ module Pv : State with type t := proofview
 module Solution : State with type t := Evd.evar_map
 
 (** Lens to the list of focused goals. *)
-module Comb : State with type t = Evar.t list
+module Comb : State with type t = goal_with_state list
 
 (** Lens to the global environment. *)
 module Env : State with type t := Environ.env
@@ -128,11 +139,11 @@ module Status : Writer with type t := bool
 
 (** Lens to the list of goals which have been shelved during the
     execution of the tactic. *)
-module Shelf : State with type t = Evar.t list
+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 = Evar.t list
+module Giveup : Writer with type t = goal list
 
 (** Lens and utilies pertaining to the info trace *)
 module InfoL : sig
-- 
cgit v1.2.3