package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
type cl_typ =
  1. | CL_SORT
  2. | CL_FUN
  3. | CL_SECVAR of Names.variable
  4. | CL_CONST of Names.Constant.t
  5. | CL_IND of Names.inductive
  6. | CL_PROJ of Names.Projection.Repr.t
val cl_typ_eq : cl_typ -> cl_typ -> bool
val subst_cl_typ : Environ.env -> Mod_subst.substitution -> cl_typ -> cl_typ
val cl_typ_ord : cl_typ -> cl_typ -> int
type cl_info_typ = {
  1. cl_param : int;
}
type coe_typ = Names.GlobRef.t
type coe_info_typ = {
  1. coe_value : Names.GlobRef.t;
  2. coe_local : bool;
  3. coe_is_identity : bool;
  4. coe_is_projection : Names.Projection.Repr.t option;
  5. coe_param : int;
}
type cl_index
type inheritance_path = coe_info_typ list
val class_exists : cl_typ -> bool
val class_info : cl_typ -> cl_index * cl_info_typ
val class_info_from_index : cl_index -> cl_typ * cl_info_typ
val inductive_class_of : Names.inductive -> cl_index
val class_args_of : Environ.env -> Evd.evar_map -> EConstr.types -> EConstr.constr list
type coercion = {
  1. coercion_type : coe_typ;
  2. coercion_local : bool;
  3. coercion_is_id : bool;
  4. coercion_is_proj : Names.Projection.Repr.t option;
  5. coercion_source : cl_typ;
  6. coercion_target : cl_typ;
  7. coercion_params : int;
}
val subst_coercion : Mod_subst.substitution -> coercion -> coercion
val declare_coercion : Environ.env -> Evd.evar_map -> coercion -> unit
val coercion_exists : coe_typ -> bool
val lookup_path_between_class : (cl_index * cl_index) -> 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 install_path_printer : (((cl_index * cl_index) * inheritance_path) -> Pp.t) -> unit
val install_path_comparator : (Environ.env -> Evd.evar_map -> cl_index -> inheritance_path -> inheritance_path -> bool) -> unit
val string_of_class : cl_typ -> string
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