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 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 conv_fun_bool = Environ.env -> Evd.evar_map -> Evd.conv_pb -> EConstr.constr -> EConstr.constr -> bool
val evar_define : conv_fun -> ?choose: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 -> conv_fun_bool -> 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) -> conv_fun -> Environ.env -> Evd.evar_map -> bool option -> EConstr.existential -> EConstr.existential -> Evd.evar_map
val solve_simple_eqn : conv_fun -> ?choose:bool -> Environ.env -> Evd.evar_map -> (bool option * EConstr.existential * EConstr.constr) -> unification_result
val reconsider_unif_constraints : conv_fun -> Evd.evar_map -> unification_result
val reconsider_conv_pbs : conv_fun -> Evd.evar_map -> unification_result
  • deprecated Alias for [reconsider_unif_constraints]
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 : Evd.evar_map -> Evar.t -> EConstr.constr -> conv_fun -> 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