package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
type opaquetab
type opaque
val empty_opaquetab : opaquetab
val create : proofterm -> opaque
val turn_indirect : Names.DirPath.t -> opaque -> opaquetab -> opaque * opaquetab
val force_proof : opaquetab -> opaque -> Constr.constr
val force_constraints : opaquetab -> opaque -> Univ.ContextSet.t
val get_constraints : opaquetab -> opaque -> Univ.ContextSet.t Future.computation option
val subst_opaque : Mod_subst.substitution -> opaque -> opaque
val iter_direct_opaque : (Constr.constr -> unit) -> opaque -> opaque
type cooking_info = {
  1. modlist : work_list;
  2. abstract : Constr.named_context * Univ.Instance.t * Univ.AUContext.t;
}
val discharge_direct_opaque : cook_constr:(Constr.constr -> Constr.constr) -> cooking_info -> opaque -> opaque
val uuid_opaque : opaquetab -> opaque -> Future.UUID.t option
val join_opaque : opaquetab -> opaque -> unit
val set_indirect_opaque_accessor : (Names.DirPath.t -> int -> Constr.constr Future.computation) -> unit
val set_indirect_univ_accessor : (Names.DirPath.t -> int -> Univ.ContextSet.t Future.computation option) -> unit
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