1 files changed, 10 insertions, 28 deletions

diff --git a/pretyping/coercionops.mli b/pretyping/coercionops.mli
index 073500b155..fb5621dd3a 100644
--- a/pretyping/coercionops.mli
+++ b/pretyping/coercionops.mli
@@ -44,12 +44,11 @@ type coe_info_typ = {
   coe_local : bool;
   coe_is_identity : bool;
   coe_is_projection : Projection.Repr.t option;
+  coe_source : cl_typ;
+  coe_target : cl_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,37 +56,21 @@ 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
 
-(** {6 [declare_coercion] adds a coercion in the graph of coercion paths } *)
-type coercion = {
-  coercion_type   : coe_typ;
-  coercion_local  : bool;
-  coercion_is_id  : bool;
-  coercion_is_proj  : Projection.Repr.t option;
-  coercion_source : cl_typ;
-  coercion_target : cl_typ;
-  coercion_params : int;
-}
-
-val subst_coercion : substitution -> coercion -> coercion
+val subst_coercion : substitution -> coe_info_typ -> coe_info_typ
 
-val declare_coercion : env -> evar_map -> coercion -> unit
+val declare_coercion : env -> evar_map -> coe_info_typ -> unit
 
 (** {6 Access to coercions infos } *)
 val coercion_exists : coe_typ -> bool
@@ -98,7 +81,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 +94,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