package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type

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 = {
  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
module P : sig ... end
module Logical : sig ... end
Lenses to access to components of the states
module type State = sig ... end
module type Reader = 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 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