diff options
Diffstat (limited to 'pretyping/coercionops.mli')
| -rw-r--r-- | pretyping/coercionops.mli | 21 |
1 files changed, 6 insertions, 15 deletions
diff --git a/pretyping/coercionops.mli b/pretyping/coercionops.mli index 073500b155..b7c46122a4 100644 --- a/pretyping/coercionops.mli +++ b/pretyping/coercionops.mli @@ -47,9 +47,6 @@ type coe_info_typ = { coe_param : int; } -(** [cl_index] is the type of class keys *) -type cl_index - (** This is the type of paths from a class to another *) type inheritance_path = coe_info_typ list @@ -57,20 +54,15 @@ type inheritance_path = coe_info_typ list val class_exists : cl_typ -> bool -val class_info : cl_typ -> (cl_index * cl_info_typ) (** @raise Not_found if this type is not a class *) - -val class_info_from_index : cl_index -> cl_typ * cl_info_typ +val class_info : cl_typ -> cl_info_typ (** [find_class_type env sigma c] returns the head reference of [c], its universe instance and its arguments *) val find_class_type : env -> evar_map -> types -> cl_typ * EInstance.t * constr list (** raises [Not_found] if not convertible to a class *) -val class_of : env -> evar_map -> types -> types * cl_index - -(** raises [Not_found] if not mapped to a class *) -val inductive_class_of : inductive -> cl_index +val class_of : env -> evar_map -> types -> types * cl_typ val class_args_of : env -> evar_map -> types -> constr list @@ -98,7 +90,7 @@ val coercion_info : coe_typ -> coe_info_typ (** @raise Not_found in the following functions when no path exists *) -val lookup_path_between_class : cl_index * cl_index -> inheritance_path +val lookup_path_between_class : cl_typ * cl_typ -> inheritance_path val lookup_path_between : env -> evar_map -> types * types -> types * types * inheritance_path val lookup_path_to_fun_from : env -> evar_map -> types -> @@ -111,16 +103,15 @@ val lookup_pattern_path_between : (**/**) (* Crade *) val install_path_printer : - ((cl_index * cl_index) * inheritance_path -> Pp.t) -> unit + ((cl_typ * cl_typ) * inheritance_path -> Pp.t) -> unit val install_path_comparator : - (env -> evar_map -> cl_index -> inheritance_path -> inheritance_path -> bool) -> unit + (env -> evar_map -> cl_typ -> inheritance_path -> inheritance_path -> bool) -> unit (**/**) (** {6 This is for printing purpose } *) 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 inheritance_graph : unit -> ((cl_typ * cl_typ) * inheritance_path) list val classes : unit -> cl_typ list val coercions : unit -> coe_info_typ list |