package coq

You can search for identifiers within the package.

in-package search v0.2.0

Package contains no libraries

type proofterm = (Term.constr * Univ.universe_context_set) Future.computation

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 get_proof : opaquetab -> opaque -> Term.constr Future.computation

val get_constraints : 
  opaquetab ->
  opaque ->
  Univ.universe_context_set Future.computation option

val subst_opaque : Mod_subst.substitution -> opaque -> opaque

val iter_direct_opaque : (Term.constr -> unit) -> opaque -> opaque

type work_list =
  (Univ.Instance.t * Names.Id.t array) Names.Cmap.t
  * (Univ.Instance.t * Names.Id.t array) Names.Mindmap.t

type cooking_info = {

modlist : work_list;
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 dump : 
  opaquetab ->
  Constr.t Future.computation array
  * Univ.universe_context_set Future.computation array
  * cooking_info list array
  * int Future.UUIDMap.t

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