Module Proofview_monadSource

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
Sourcemodule Trace : sig ... end
State types
Sourcetype 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.

Sourcemodule Info : sig ... end

Info trace.

Sourcetype goal = Evar.t
Sourcetype goal_with_state
Sourceval drop_state : goal_with_state -> goal
Sourceval goal_with_state : goal -> StateStore.t -> goal_with_state
Sourceval with_empty_state : goal -> goal_with_state
Sourceval map_goal_with_state : (goal -> goal) -> goal_with_state -> goal_with_state
Sourcetype proofview = {
  1. solution : Evd.evar_map;
  2. comb : goal_with_state list;
}

Type of proof views: current evar_map together with the list of focused goals, locally shelved goals and globally shelved goals.

Instantiation of the logic monad
Sourcemodule P : sig ... end
Sourcemodule Logical : sig ... end
Lenses to access to components of the states
Sourcemodule type State = sig ... end
Sourcemodule type Reader = sig ... end
Sourcemodule type Writer = sig ... end
Sourcemodule Pv : State with type t := proofview

Lens to the proofview.

Sourcemodule Solution : State with type t := Evd.evar_map

Lens to the evar_map of the proofview.

Sourcemodule Comb : State with type t = goal_with_state list

Lens to the list of focused goals.

Sourcemodule Env : State with type t := Environ.env

Lens to the global environment.

Sourcemodule Status : Writer with type t := bool

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

Sourcemodule InfoL : sig ... end

Lens and utilities pertaining to the info trace