Module Classops

type cl_typ =
| CL_SORT
| CL_FUN
| CL_SECVAR of Names.variable
| CL_CONST of Names.Constant.t
| CL_IND of Names.inductive
| CL_PROJ of Names.Projection.Repr.t
This is the type of class kinds
val cl_typ_eq : cl_typ -> cl_typ -> bool

Equality over cl_typ

val subst_cl_typ : Mod_subst.substitution -> cl_typ -> cl_typ
val cl_typ_ord : cl_typ -> cl_typ -> int

Comparison of cl_typ

type cl_info_typ = {
cl_param : int;
}

This is the type of infos for declared classes

type coe_typ = Names.GlobRef.t

This is the type of coercion kinds

type coe_info_typ = {
coe_value : Names.GlobRef.t;
coe_local : bool;
coe_is_identity : bool;
coe_is_projection : Names.Projection.Repr.t option;
coe_param : int;
}

This is the type of infos for declared coercions

type cl_index

cl_index is the type of class keys

type inheritance_path = coe_info_typ list

This is the type of paths from a class to another

Access to classes infos
val class_exists : cl_typ -> bool
val class_info : cl_typ -> cl_index * cl_info_typ
raises Not_found

if this type is not a class

val class_info_from_index : cl_index -> cl_typ * cl_info_typ
val find_class_type : Evd.evar_map -> EConstr.types -> cl_typ * EConstr.EInstance.t * EConstr.constr list

find_class_type env sigma c returns the head reference of c, its universe instance and its arguments

val class_of : Environ.env -> Evd.evar_map -> EConstr.types -> EConstr.types * cl_index

raises Not_found if not convertible to a class

val inductive_class_of : Names.inductive -> cl_index

raises Not_found if not mapped to a class

val class_args_of : Environ.env -> Evd.evar_map -> EConstr.types -> EConstr.constr list
type coercion = {
coercion_type : coe_typ;
coercion_local : bool;
coercion_is_id : bool;
coercion_is_proj : Names.Projection.Repr.t option;
coercion_source : cl_typ;
coercion_target : cl_typ;
coercion_params : int;
}
declare_coercion adds a coercion in the graph of coercion paths
val subst_coercion : Mod_subst.substitution -> coercion -> coercion
val declare_coercion : Environ.env -> Evd.evar_map -> coercion -> unit
val coercion_exists : coe_typ -> bool
Access to coercions infos
Lookup functions for coercion paths
val lookup_path_between_class : (cl_index * cl_index) -> inheritance_path
val lookup_path_between : Environ.env -> Evd.evar_map -> (EConstr.types * EConstr.types) -> EConstr.types * EConstr.types * inheritance_path
val lookup_path_to_fun_from : Environ.env -> Evd.evar_map -> EConstr.types -> EConstr.types * inheritance_path
val lookup_path_to_sort_from : Environ.env -> Evd.evar_map -> EConstr.types -> EConstr.types * inheritance_path
val lookup_pattern_path_between : Environ.env -> (Names.inductive * Names.inductive) -> (Names.constructor * int) list
val string_of_class : cl_typ -> string
This is for printing purpose
val pr_class : cl_typ -> Pp.t
val pr_cl_index : cl_index -> Pp.t
val inheritance_graph : unit -> ((cl_index * cl_index) * inheritance_path) list
val classes : unit -> cl_typ list
val coercions : unit -> coe_info_typ list
val hide_coercion : coe_typ -> int option

hide_coercion returns the number of params to skip if the coercion must be hidden, None otherwise; it raises Not_found if not a coercion