package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
type direction =
  1. | Forward
  2. | Backward
type !'a hint_info_gen = {
  1. hint_priority : int option;
  2. hint_pattern : 'a option;
}
type typeclass = {
  1. cl_univs : Univ.AUContext.t;
  2. cl_impl : Names.GlobRef.t;
  3. cl_context : Names.GlobRef.t option list * Constr.rel_context;
  4. cl_props : Constr.rel_context;
  5. cl_projs : (Names.Name.t * (direction * hint_info) option * Names.Constant.t option) list;
  6. cl_strict : bool;
  7. cl_unique : bool;
}
type instance
val instances : Names.GlobRef.t -> instance list
val typeclasses : unit -> typeclass list
val all_instances : unit -> instance list
val add_class : typeclass -> unit
val new_instance : typeclass -> hint_info -> bool -> Names.GlobRef.t -> instance
val add_instance : instance -> unit
val remove_instance : instance -> unit
val class_info : Names.GlobRef.t -> typeclass
val typeclass_univ_instance : typeclass Univ.puniverses -> typeclass
val instance_impl : instance -> Names.GlobRef.t
val hint_priority : instance -> int option
val is_class : Names.GlobRef.t -> bool
val is_instance : Names.GlobRef.t -> bool
val instance_constructor : typeclass EConstr.puniverses -> EConstr.t list -> EConstr.t option * EConstr.t
type evar_filter = Evar.t -> Evar_kinds.t -> bool
val all_evars : evar_filter
val all_goals : evar_filter
val no_goals : evar_filter
val no_goals_or_obligations : evar_filter
val set_resolvable : Evd.Store.t -> bool -> Evd.Store.t
val is_resolvable : Evd.evar_info -> bool
val mark_unresolvable : Evd.evar_info -> Evd.evar_info
val mark_unresolvables : ?filter:evar_filter -> Evd.evar_map -> Evd.evar_map
val mark_resolvables : ?filter:evar_filter -> Evd.evar_map -> Evd.evar_map
val mark_resolvable : Evd.evar_info -> Evd.evar_info
val is_class_evar : Evd.evar_map -> Evd.evar_info -> bool
val is_class_type : Evd.evar_map -> EConstr.types -> bool
val resolve_typeclasses : ?fast_path:bool -> ?filter:evar_filter -> ?unique:bool -> ?split:bool -> ?fail:bool -> Environ.env -> Evd.evar_map -> Evd.evar_map
val resolve_one_typeclass : ?unique:bool -> Environ.env -> Evd.evar_map -> EConstr.types -> Evd.evar_map * EConstr.constr
val set_typeclass_transparency_hook : (Names.evaluable_global_reference -> bool -> bool -> unit) Hook.t
val set_typeclass_transparency : Names.evaluable_global_reference -> bool -> bool -> unit
val classes_transparent_state_hook : (unit -> Names.transparent_state) Hook.t
val classes_transparent_state : unit -> Names.transparent_state
val add_instance_hint_hook : (Globnames.global_reference_or_constr -> Names.GlobRef.t list -> bool -> hint_info -> Decl_kinds.polymorphic -> unit) Hook.t
val remove_instance_hint_hook : (Names.GlobRef.t -> unit) Hook.t
val add_instance_hint : Globnames.global_reference_or_constr -> Names.GlobRef.t list -> bool -> hint_info -> Decl_kinds.polymorphic -> unit
val remove_instance_hint : Names.GlobRef.t -> unit
val solve_all_instances_hook : (Environ.env -> Evd.evar_map -> evar_filter -> bool -> bool -> bool -> Evd.evar_map) Hook.t
val solve_one_instance_hook : (Environ.env -> Evd.evar_map -> EConstr.types -> bool -> Evd.evar_map * EConstr.constr) Hook.t
val declare_instance : hint_info option -> bool -> Names.GlobRef.t -> unit
val build_subclasses : check:bool -> Environ.env -> Evd.evar_map -> Names.GlobRef.t -> hint_info -> (Names.GlobRef.t list * hint_info * Constr.constr) list