From 041ee4822cb247e60df51fa147175f8b16711df1 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 22 Jan 2018 17:35:02 +0100 Subject: proofview: goals come with a state --- engine/proofview_monad.mli | 21 +++++++++++++++------ 1 file changed, 15 insertions(+), 6 deletions(-) (limited to 'engine/proofview_monad.mli') diff --git a/engine/proofview_monad.mli b/engine/proofview_monad.mli index e7123218b..d26816fa6 100644 --- a/engine/proofview_monad.mli +++ b/engine/proofview_monad.mli @@ -67,12 +67,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 +90,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 +127,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 +137,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