package coq

You can search for identifiers within the package.

in-package search v0.2.0

Package contains no libraries

type proofterm = (Constr.constr * Univ.ContextSet.t) 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 -> Constr.constr

val force_constraints : opaquetab -> opaque -> Univ.ContextSet.t

val get_proof : opaquetab -> opaque -> Constr.constr Future.computation

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

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