package coq

  1. Overview
  2. Docs
Legend:
Library
Module
Module type
Parameter
Class
Class type
val add_bidirectionality_hint : Names.GlobRef.t -> int -> unit
val get_bidirectionality_hint : Names.GlobRef.t -> int option
val clear_bidirectionality_hint : Names.GlobRef.t -> unit
val interp_known_glob_level : ?loc:Loc.t -> Evd.evar_map -> Glob_term.glob_sort_name -> Univ.Level.t
val search_guard : ?loc:Loc.t -> Environ.env -> int list list -> Constr.rec_declaration -> int array
type typing_constraint =
  1. | UnknownIfTermOrType
  2. | IsType
  3. | OfType of EConstr.types
  4. | WithoutTypeConstraint
type use_typeclasses =
  1. | NoUseTC
  2. | UseTCForConv
  3. | UseTC
type inference_flags = {
  1. use_typeclasses : use_typeclasses;
  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
type inference_hook = Environ.env -> Evd.evar_map -> Evar.t -> (Evd.evar_map * EConstr.constr) option
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 -> ?initial:Evd.evar_map -> Evd.evar_map -> EConstr.constr -> unit
type !'a pretype_fun = ?loc:Loc.t -> program_mode:bool -> poly:bool -> bool -> Evardefine.type_constraint -> GlobEnv.t -> Evd.evar_map -> Evd.evar_map * 'a
type pretyper = {
  1. pretype_ref : pretyper -> (Names.GlobRef.t * Glob_term.glob_level list option) -> EConstr.unsafe_judgment pretype_fun;
  2. pretype_var : pretyper -> Names.Id.t -> EConstr.unsafe_judgment pretype_fun;
  3. pretype_evar : pretyper -> (Glob_term.existential_name * (Names.Id.t * Glob_term.glob_constr) list) -> EConstr.unsafe_judgment pretype_fun;
  4. pretype_patvar : pretyper -> Evar_kinds.matching_var_kind -> EConstr.unsafe_judgment pretype_fun;
  5. pretype_app : pretyper -> (Glob_term.glob_constr * Glob_term.glob_constr list) -> EConstr.unsafe_judgment pretype_fun;
  6. pretype_lambda : pretyper -> (Names.Name.t * Glob_term.binding_kind * Glob_term.glob_constr * Glob_term.glob_constr) -> EConstr.unsafe_judgment pretype_fun;
  7. pretype_prod : pretyper -> (Names.Name.t * Glob_term.binding_kind * Glob_term.glob_constr * Glob_term.glob_constr) -> EConstr.unsafe_judgment pretype_fun;
  8. pretype_letin : pretyper -> (Names.Name.t * Glob_term.glob_constr * Glob_term.glob_constr option * Glob_term.glob_constr) -> EConstr.unsafe_judgment pretype_fun;
  9. pretype_cases : pretyper -> (Constr.case_style * Glob_term.glob_constr option * Glob_term.tomatch_tuples * Glob_term.cases_clauses) -> EConstr.unsafe_judgment pretype_fun;
  10. pretype_lettuple : pretyper -> (Names.Name.t list * (Names.Name.t * Glob_term.glob_constr option) * Glob_term.glob_constr * Glob_term.glob_constr) -> EConstr.unsafe_judgment pretype_fun;
  11. pretype_if : pretyper -> (Glob_term.glob_constr * (Names.Name.t * Glob_term.glob_constr option) * Glob_term.glob_constr * Glob_term.glob_constr) -> EConstr.unsafe_judgment pretype_fun;
  12. pretype_rec : pretyper -> (Glob_term.glob_fix_kind * Names.Id.t array * Glob_term.glob_decl list array * Glob_term.glob_constr array * Glob_term.glob_constr array) -> EConstr.unsafe_judgment pretype_fun;
  13. pretype_sort : pretyper -> Glob_term.glob_sort -> EConstr.unsafe_judgment pretype_fun;
  14. pretype_hole : pretyper -> (Evar_kinds.t * Namegen.intro_pattern_naming_expr * Genarg.glob_generic_argument option) -> EConstr.unsafe_judgment pretype_fun;
  15. pretype_cast : pretyper -> (Glob_term.glob_constr * Glob_term.glob_constr Glob_term.cast_type) -> EConstr.unsafe_judgment pretype_fun;
  16. pretype_int : pretyper -> Uint63.t -> EConstr.unsafe_judgment pretype_fun;
  17. pretype_float : pretyper -> Float64.t -> EConstr.unsafe_judgment pretype_fun;
  18. pretype_type : pretyper -> Glob_term.glob_constr -> EConstr.unsafe_type_judgment pretype_fun;
}
val default_pretyper : pretyper
val eval_pretyper : pretyper -> program_mode:bool -> poly:bool -> bool -> Evardefine.type_constraint -> GlobEnv.t -> Evd.evar_map -> Glob_term.glob_constr -> Evd.evar_map * EConstr.unsafe_judgment
OCaml

Innovation. Community. Security.