package coq

  1. Overview
  2. Docs
Legend:
Library
Module
Module type
Parameter
Class
Class type
val mismatched_params : Environ.env -> Constrexpr.constr_expr list -> Context.Rel.t -> 'a
val mismatched_props : Environ.env -> Constrexpr.constr_expr list -> Context.Rel.t -> 'a
val existing_instance : bool -> Libnames.reference -> Vernacexpr.hint_info_expr option -> unit
val declare_instance_constant : Typeclasses.typeclass -> Vernacexpr.hint_info_expr -> bool -> Impargs.manual_explicitation list -> ?hook:(Globnames.global_reference -> unit) -> Names.Id.t -> Names.Id.t Loc.located list option -> bool -> Evd.evar_map -> Constr.t -> Term.types -> Names.Id.t
val new_instance : ?abstract:bool -> ?global:bool -> ?refine:bool -> Decl_kinds.polymorphic -> Constrexpr.local_binder_expr list -> Constrexpr.typeclass_constraint -> (bool * Constrexpr.constr_expr) option -> ?generalize:bool -> ?tac:unit Proofview.tactic -> ?hook:(Globnames.global_reference -> unit) -> Vernacexpr.hint_info_expr -> Names.Id.t
val set_typeclass_transparency : Names.evaluable_global_reference -> bool -> bool -> unit
val id_of_class : Typeclasses.typeclass -> Names.Id.t
OCaml

Innovation. Community. Security.