package coq

  1. Overview
  2. Docs
Legend:
Library
Module
Module type
Parameter
Class
Class type
val search_guard : ?loc:Loc.t -> Environ.env -> int list list -> Term.rec_declaration -> int array
type typing_constraint =
  1. | OfType of EConstr.types
  2. | IsType
  3. | WithoutTypeConstraint
type glob_constr_ltac_closure = Glob_term.ltac_var_map * Glob_term.glob_constr
type pure_open_constr = Evd.evar_map * EConstr.constr
type inference_flags = {
  1. use_typeclasses : bool;
  2. solve_unification_constraints : bool;
  3. use_hook : inference_hook option;
  4. fail_evar : bool;
  5. expand_evars : bool;
}
val default_inference_flags : bool -> inference_flags
val no_classes_no_fail_inference_flags : inference_flags
val all_no_fail_flags : inference_flags
val all_and_fail_flags : inference_flags
val allow_anonymous_refs : bool ref
val understand_tcc_evars : ?flags:inference_flags -> Environ.env -> Evd.evar_map ref -> ?expected_type:typing_constraint -> Glob_term.glob_constr -> EConstr.constr
val solve_remaining_evars : inference_flags -> Environ.env -> Evd.evar_map -> Evd.evar_map -> Evd.evar_map
val check_evars_are_solved : Environ.env -> Evd.evar_map -> Evd.evar_map -> unit
val check_evars : Environ.env -> Evd.evar_map -> Evd.evar_map -> EConstr.constr -> unit
val interp_elimination_sort : Misctypes.glob_sort -> Term.sorts_family
val register_constr_interp0 : ('r, 'g, 't) Genarg.genarg_type -> (Glob_term.unbound_ltac_var_map -> Environ.env -> Evd.evar_map -> EConstr.types -> 'g -> EConstr.constr * Evd.evar_map) -> unit
OCaml

Innovation. Community. Security.