coq 8.7.2 · OCaml Package

type cl_typ =

val cl_typ_eq : cl_typ -> cl_typ -> bool

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

val cl_typ_ord : cl_typ -> cl_typ -> int

type cl_info_typ = {

}

type coe_typ = Globnames.global_reference

type coe_info_typ

type cl_index

type coe_index

type inheritance_path = coe_index 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 find_class_type : 
  Evd.evar_map ->
  EConstr.types ->
  cl_typ * EConstr.EInstance.t * EConstr.constr list

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

val inductive_class_of : Names.inductive -> cl_index

val class_args_of : 
  Environ.env ->
  Evd.evar_map ->
  EConstr.types ->
  EConstr.constr list

val declare_coercion : 
  coe_typ ->
  ?local:bool ->
  isid:bool ->
  src:cl_typ ->
  target:cl_typ ->
  params:int ->
  unit

val coercion_exists : coe_typ -> bool

val coercion_value : 
  coe_index ->
  (EConstr.unsafe_judgment * bool * bool) Univ.in_universe_context_set

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 install_path_printer : 
  (((cl_index * cl_index) * inheritance_path) -> Pp.std_ppcmds) ->
  unit

val string_of_class : cl_typ -> string

val pr_class : cl_typ -> Pp.std_ppcmds

val pr_cl_index : cl_index -> Pp.std_ppcmds

val get_coercion_value : coe_index -> Constr.t

val inheritance_graph : unit -> ((cl_index * cl_index) * inheritance_path) list

val classes : unit -> cl_typ list

val coercions : unit -> coe_index list

val hide_coercion : coe_typ -> int option

package coq