package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
type coercion_trace
val empty_coercion_trace : coercion_trace
val reapply_coercions : Evd.evar_map -> coercion_trace -> EConstr.t -> EConstr.t
val inh_app_fun : program_mode:bool -> bool -> Environ.env -> Evd.evar_map -> EConstr.unsafe_judgment -> Evd.evar_map * EConstr.unsafe_judgment * coercion_trace
val inh_coerce_to_base : ?loc:Loc.t -> program_mode:bool -> Environ.env -> Evd.evar_map -> EConstr.unsafe_judgment -> Evd.evar_map * EConstr.unsafe_judgment
val inh_coerce_to_prod : ?loc:Loc.t -> program_mode:bool -> Environ.env -> Evd.evar_map -> EConstr.types -> Evd.evar_map * EConstr.types
val inh_conv_coerce_to : ?loc:Loc.t -> program_mode:bool -> bool -> Environ.env -> Evd.evar_map -> ?flags:Evarconv.unify_flags -> EConstr.unsafe_judgment -> EConstr.types -> Evd.evar_map * EConstr.unsafe_judgment * coercion_trace option
val inh_conv_coerce_rigid_to : ?loc:Loc.t -> program_mode:bool -> bool -> Environ.env -> Evd.evar_map -> ?flags:Evarconv.unify_flags -> EConstr.unsafe_judgment -> EConstr.types -> Evd.evar_map * EConstr.unsafe_judgment * coercion_trace option