package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
val declare_instance : ?warn:bool -> Environ.env -> Evd.evar_map -> Typeclasses.hint_info option -> bool -> Names.GlobRef.t -> unit
val existing_instance : bool -> Libnames.qualid -> Vernacexpr.hint_info_expr option -> unit
val new_instance_interactive : ?global:bool -> poly:bool -> Constrexpr.name_decl -> Constrexpr.local_binder_expr list -> Constrexpr.constr_expr -> ?generalize:bool -> ?tac:unit Proofview.tactic -> ?hook:(Names.GlobRef.t -> unit) -> Vernacexpr.hint_info_expr -> (bool * Constrexpr.constr_expr) option -> Names.Id.t * Declare.Proof.t
val new_instance : ?global:bool -> poly:bool -> Constrexpr.name_decl -> Constrexpr.local_binder_expr list -> Constrexpr.constr_expr -> (bool * Constrexpr.constr_expr) -> ?generalize:bool -> ?hook:(Names.GlobRef.t -> unit) -> Vernacexpr.hint_info_expr -> Names.Id.t
val new_instance_program : ?global:bool -> pm:Declare.OblState.t -> poly:bool -> Constrexpr.name_decl -> Constrexpr.local_binder_expr list -> Constrexpr.constr_expr -> (bool * Constrexpr.constr_expr) option -> ?generalize:bool -> ?hook:(Names.GlobRef.t -> unit) -> Vernacexpr.hint_info_expr -> Declare.OblState.t * Names.Id.t
val declare_new_instance : ?global:bool -> program_mode:bool -> poly:bool -> Constrexpr.ident_decl -> Constrexpr.local_binder_expr list -> Constrexpr.constr_expr -> Vernacexpr.hint_info_expr -> unit
val add_instance : Typeclasses.instance -> unit
val add_class : Environ.env -> Evd.evar_map -> Typeclasses.typeclass -> unit
val set_typeclass_transparency : Names.evaluable_global_reference -> bool -> bool -> unit
val id_of_class : Typeclasses.typeclass -> Names.Id.t
val refine_att : bool Attributes.attribute