diff options
| -rw-r--r-- | pretyping/coercionops.ml | 6 | ||||
| -rw-r--r-- | pretyping/coercionops.mli | 16 | ||||
| -rw-r--r-- | pretyping/pretyping.ml | 2 |
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}) |