Module Proofview_monad
This file defines the datatypes used as internal states by the tactic monad, and specialises the Logic_monad
to these types. It should not be used directly. Consider using Proofview
instead.
Traces
module Trace : sig ... end
State types
type lazy_msg
= Environ.env -> Evd.evar_map -> Pp.t
We typically label nodes of
Trace.tree
with messages to print. But we don't want to compute the result.
module Info : sig ... end
Info trace.
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 proofview
=
{
solution : Evd.evar_map;
comb : goal_with_state list;
shelf : goal list;
}
Type of proof views: current
evar_map
together with the list of focused goals.
Instantiation of the logic monad
module P : sig ... end
module Logical : module type of sig ... end
Lenses to access to components of the states
module type State = sig ... end
module type Writer = sig ... end
module Solution : State with type t := Evd.evar_map
Lens to the
evar_map
of the proofview.
module Comb : State with type t = goal_with_state list
Lens to the list of focused goals.
module Env : State with type t := Environ.env
Lens to the global environment.
module Shelf : State with type t = goal list
Lens to the list of goals which have been shelved during the execution of the tactic.
module Giveup : Writer with type t = goal list
Lens to the list of goals which were given up during the execution of the tactic.
module InfoL : sig ... end
Lens and utilities pertaining to the info trace