From 4bbbaff29bb748800636c7c737fdbda3a2ee819d Mon Sep 17 00:00:00 2001
From: Kazuhiko Sakaguchi
Date: Sat, 6 Mar 2021 22:19:41 +0900
Subject: Replace cl_index with cl_typ in coercionops.ml

The table of coercion classes `class_tab` is now indexed by `cl_typ` instead of
integers (`cl_index`). All the uses of `cl_index` and `Bijint` have been
replaced with `cl_typ` and `ClTypMap` respectively.
---
 pretyping/coercionops.mli | 21 ++++++---------------
 1 file changed, 6 insertions(+), 15 deletions(-)

(limited to 'pretyping/coercionops.mli')

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
 
-- 
cgit v1.2.3