package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
module Trace : sig ... end
type lazy_msg = unit -> Pp.t
module Info : sig ... end
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;
  3. shelf : goal list;
}
module P : sig ... end
module Logical : sig ... end
module type State = sig ... end
module type Writer = sig ... end
module Pv : sig ... end
module Solution : sig ... end
module Comb : sig ... end
module Env : sig ... end
module Status : sig ... end
module Shelf : sig ... end
module Giveup : sig ... end
module InfoL : sig ... end
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