package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
val interp_known_glob_level : ?loc:Loc.t -> Evd.evar_map -> Glob_term.glob_level -> Univ.Level.t
val search_guard : ?loc:Loc.t -> Environ.env -> int list list -> Constr.rec_declaration -> int array
type typing_constraint =
  1. | OfType of EConstr.types
  2. | IsType
  3. | WithoutTypeConstraint
type inference_hook = Environ.env -> Evd.evar_map -> Evar.t -> 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 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 register_constr_interp0 : ('r, 'g, 't) Genarg.genarg_type -> (Ltac_pretype.unbound_ltac_var_map -> Environ.env -> Evd.evar_map -> EConstr.types -> 'g -> EConstr.constr * Evd.evar_map) -> unit