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