package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
val declare_generalizable : local:bool -> Names.lident list option -> unit
val ids_of_list : Names.Id.t list -> Names.Id.Set.t
val free_vars_of_constr_expr : Constrexpr.constr_expr -> ?bound:Names.Id.Set.t -> Names.Id.t list -> Names.Id.t list
val free_vars_of_binders : ?bound:Names.Id.Set.t -> Names.Id.t list -> Constrexpr.local_binder_expr list -> Names.Id.Set.t * Names.Id.t list
val generalizable_vars_of_glob_constr : ?bound:Names.Id.Set.t -> ?allowed:Names.Id.Set.t -> Glob_term.glob_constr -> Names.lident list
val implicits_of_glob_constr : ?with_products:bool -> Glob_term.glob_constr -> Impargs.manual_implicits
exception MismatchedContextInstance of Environ.env * Typeclasses_errors.contexts * Constrexpr.constr_expr list * Constr.rel_context
val mismatched_ctx_inst_err : Environ.env -> Typeclasses_errors.contexts -> Constrexpr.constr_expr list -> Constr.rel_context -> 'a