diff options
Diffstat (limited to 'pretyping/classops.mli')
| -rw-r--r-- | pretyping/classops.mli | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/pretyping/classops.mli b/pretyping/classops.mli index cf88be62..d509739c 100644 --- a/pretyping/classops.mli +++ b/pretyping/classops.mli @@ -26,6 +26,9 @@ val cl_typ_eq : cl_typ -> cl_typ -> bool val subst_cl_typ : substitution -> cl_typ -> cl_typ +(** Comparison of [cl_typ] *) +val cl_typ_ord : cl_typ -> cl_typ -> int + (** This is the type of infos for declared classes *) type cl_info_typ = { cl_param : int } |