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.

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 Pv : State with type t := proofview

Lens to the proofview.

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 Status : Writer with type t := bool

Lens to the tactic status (true if safe, false if unsafe)

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