package coq-core

  1. Overview
  2. Docs
package coq-core
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

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 = unit -> 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

OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct