package coq

  1. Overview
  2. Docs
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 -> Term.constr
val force_constraints : opaquetab -> opaque -> Univ.universe_context_set
val subst_opaque : Mod_subst.substitution -> opaque -> opaque
val iter_direct_opaque : (Term.constr -> unit) -> opaque -> opaque
type cooking_info = {
  1. modlist : work_list;
  2. abstract : Context.Named.t * Univ.universe_level_subst * Univ.AUContext.t;
}
val discharge_direct_opaque : cook_constr:(Term.constr -> Term.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 -> Term.constr Future.computation) -> unit
val set_indirect_univ_accessor : (Names.DirPath.t -> int -> Univ.universe_context_set Future.computation option) -> unit
OCaml

Innovation. Community. Security.