coq 8.7.1 · OCaml Package

coq

type direction =

| Forward
| Backward

type typeclass = {

cl_impl : Globnames.global_reference;
cl_context : (Globnames.global_reference * bool) option list * Context.Rel.t;
cl_props : Context.Rel.t;
cl_projs : (Names.Name.t * (direction * Vernacexpr.hint_info_expr) option * Names.constant option) list;
cl_strict : bool;
cl_unique : bool;

}

type instance

val instances : Globnames.global_reference -> instance list

val typeclasses : unit -> typeclass list

val all_instances : unit -> instance list

val add_class : typeclass -> unit

val new_instance : 
  typeclass ->
  Vernacexpr.hint_info_expr ->
  bool ->
  Decl_kinds.polymorphic ->
  Globnames.global_reference ->
  instance

val add_instance : instance -> unit

val remove_instance : instance -> unit

val class_info : Globnames.global_reference -> typeclass

val dest_class_app : 
  Environ.env ->
  Evd.evar_map ->
  EConstr.constr ->
  (typeclass * EConstr.EInstance.t) * Term.constr list

val typeclass_univ_instance : 
  typeclass Term.puniverses ->
  typeclass Term.puniverses

val class_of_constr : 
  Evd.evar_map ->
  EConstr.constr ->
  (EConstr.rel_context * ((typeclass * EConstr.EInstance.t) * Term.constr list))
    option

val instance_impl : instance -> Globnames.global_reference

val hint_priority : instance -> int option

val is_class : Globnames.global_reference -> bool

val is_instance : Globnames.global_reference -> bool

val instance_constructor : 
  typeclass Term.puniverses ->
  Term.constr list ->
  Term.constr option * Term.types

type evar_filter = Term.existential_key -> 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 ->
    Globnames.global_reference list ->
    bool ->
    Vernacexpr.hint_info_expr ->
    Decl_kinds.polymorphic ->
    unit)
    Hook.t

val remove_instance_hint_hook : (Globnames.global_reference -> unit) Hook.t

val add_instance_hint : 
  Globnames.global_reference_or_constr ->
  Globnames.global_reference list ->
  bool ->
  Vernacexpr.hint_info_expr ->
  Decl_kinds.polymorphic ->
  unit

val remove_instance_hint : Globnames.global_reference -> 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 : 
  Vernacexpr.hint_info_expr option ->
  bool ->
  Globnames.global_reference ->
  unit

val build_subclasses : 
  check:bool ->
  Environ.env ->
  Evd.evar_map ->
  Globnames.global_reference ->
  Vernacexpr.hint_info_expr ->
  (Globnames.global_reference list * Vernacexpr.hint_info_expr * Term.constr)
    list

package coq