Expose less interface in coercionops.mli

3 files changed, 8 insertions, 16 deletions

diff --git a/pretyping/coercionops.ml b/pretyping/coercionops.ml
index 8b864b4dd3..9b25d63640 100644
--- a/pretyping/coercionops.ml
+++ b/pretyping/coercionops.ml
@@ -57,9 +57,13 @@ module ClTypMap = Map.Make(ClTyp)
 module ClPairMap = Map.Make(ClPairOrd)
 
 type cl_info_typ = {
+  (* The number of parameters of the coercion class. *)
   cl_param : int;
+  (* The sets of coercion classes respectively reachable from and to the
+     coercion class. *)
   cl_reachable_from : ClTypSet.t;
   cl_reachable_to : ClTypSet.t;
+  (* The representative class of the strongly connected component. *)
   cl_repr : cl_typ;
 }
 
@@ -114,6 +118,8 @@ let add_new_path x y =
 
 let class_info cl = ClTypMap.find cl !class_tab
 
+let class_nparams cl = (class_info cl).cl_param
+
 let class_exists cl = ClTypMap.mem cl !class_tab
 
 let coercion_info coe = CoeTypMap.find coe !coercion_tab
diff --git a/pretyping/coercionops.mli b/pretyping/coercionops.mli
index 9236167021..af91dd1d0e 100644
--- a/pretyping/coercionops.mli
+++ b/pretyping/coercionops.mli
@@ -31,20 +31,6 @@ val subst_cl_typ : env -> substitution -> cl_typ -> cl_typ
 (** Comparison of [cl_typ] *)
 val cl_typ_ord : cl_typ -> cl_typ -> int
 
-module ClTypSet : Set.S with type elt = cl_typ
-
-(** This is the type of infos for declared classes *)
-type cl_info_typ = {
-  (* The number of parameters of the coercion class. *)
-  cl_param : int;
-  (* The sets of coercion classes respectively reachable from and to the
-     coercion class. *)
-  cl_reachable_from : ClTypSet.t;
-  cl_reachable_to : ClTypSet.t;
-  (* The representative class of the strongly connected component. *)
-  cl_repr : cl_typ;
-}
-
 (** This is the type of coercion kinds *)
 type coe_typ = GlobRef.t
 
@@ -67,7 +53,7 @@ type inheritance_path = coe_info_typ list
 val class_exists : cl_typ -> bool
 
 (** @raise Not_found if this type is not a class *)
-val class_info : cl_typ -> cl_info_typ
+val class_nparams : cl_typ -> int
 
 (** [find_class_type env sigma c] returns the head reference of [c],
     its universe instance and its arguments *)
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 3ccc6ea125..4f9283e999 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -1423,7 +1423,7 @@ let path_convertible env sigma cl p q =
           p'
     | [] ->
       (* identity function for the class [i]. *)
-      let params = (class_info cl).cl_param in
+      let params = class_nparams cl in
       let clty =
         match cl with
         | CL_SORT -> mkGSort (Glob_term.UAnonymous {rigid=false})