package coq

  1. Overview
  2. Docs
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. fail_evar : bool;
  4. expand_evars : bool;
  5. program_mode : bool;
  6. polymorphic : 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 : ?hook:inference_hook -> inference_flags -> Environ.env -> ?initial:Evd.evar_map -> Evd.evar_map -> Evd.evar_map
val check_evars_are_solved : program_mode:bool -> Environ.env -> ?initial:Evd.evar_map -> Evd.evar_map -> unit
val check_evars : Environ.env -> Evd.evar_map -> Evd.evar_map -> EConstr.constr -> unit
OCaml

Innovation. Community. Security.