package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
type alias
val of_alias : alias -> EConstr.t
type unify_flags = {
  1. modulo_betaiota : bool;
  2. open_ts : TransparentState.t;
  3. closed_ts : TransparentState.t;
  4. subterm_ts : TransparentState.t;
  5. frozen_evars : Evar.Set.t;
  6. allow_K_at_toplevel : bool;
  7. with_cs : bool;
}
type unification_result =
  1. | Success of Evd.evar_map
  2. | UnifFailure of Evd.evar_map * Pretype_errors.unification_error
val is_success : unification_result -> bool
val expand_vars_in_term : Environ.env -> Evd.evar_map -> EConstr.constr -> EConstr.constr
type unification_kind =
  1. | TypeUnification
  2. | TermUnification
val instantiate_evar : unifier -> unify_flags -> Evd.evar_map -> Evar.t -> EConstr.constr -> Evd.evar_map
val evar_define : unifier -> unify_flags -> ?choose:bool -> ?imitate_defs:bool -> Environ.env -> Evd.evar_map -> bool option -> EConstr.existential -> EConstr.constr -> Evd.evar_map
val refresh_universes : ?status:Evd.rigid -> ?onlyalg:bool -> ?refreshset:bool -> bool option -> Environ.env -> Evd.evar_map -> EConstr.types -> Evd.evar_map * EConstr.types
val solve_refl : ?can_drop:bool -> conversion_check -> unify_flags -> Environ.env -> Evd.evar_map -> bool option -> Evar.t -> EConstr.constr array -> EConstr.constr array -> Evd.evar_map
val solve_evar_evar : ?force:bool -> (Environ.env -> Evd.evar_map -> bool option -> EConstr.existential -> EConstr.constr -> Evd.evar_map) -> unifier -> unify_flags -> Environ.env -> Evd.evar_map -> bool option -> EConstr.existential -> EConstr.existential -> Evd.evar_map
val solve_simple_eqn : unifier -> unify_flags -> ?choose:bool -> ?imitate_defs:bool -> Environ.env -> Evd.evar_map -> (bool option * EConstr.existential * EConstr.constr) -> unification_result
val reconsider_unif_constraints : unifier -> unify_flags -> Evd.evar_map -> unification_result
val is_unification_pattern_evar : Environ.env -> Evd.evar_map -> EConstr.existential -> EConstr.constr list -> EConstr.constr -> alias list option
val is_unification_pattern : (Environ.env * int) -> Evd.evar_map -> EConstr.constr -> EConstr.constr list -> EConstr.constr -> alias list option
val solve_pattern_eqn : Environ.env -> Evd.evar_map -> alias list -> EConstr.constr -> EConstr.constr
val noccur_evar : Environ.env -> Evd.evar_map -> Evar.t -> EConstr.constr -> bool
exception IllTypedInstance of Environ.env * EConstr.types * EConstr.types
val check_evar_instance : unifier -> unify_flags -> Evd.evar_map -> Evar.t -> EConstr.constr -> Evd.evar_map
val remove_instance_local_defs : Evd.evar_map -> Evar.t -> 'a array -> 'a list
val get_type_of_refresh : ?polyprop:bool -> ?lax:bool -> Environ.env -> Evd.evar_map -> EConstr.constr -> Evd.evar_map * EConstr.types
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct