diff options
Diffstat (limited to 'engine/proofview_monad.mli')
| -rw-r--r-- | engine/proofview_monad.mli | 35 |
1 files changed, 23 insertions, 12 deletions
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 |