aboutsummaryrefslogtreecommitdiff
path: root/pretyping
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping')
-rw-r--r--pretyping/classops.mli3
1 files changed, 2 insertions, 1 deletions
diff --git a/pretyping/classops.mli b/pretyping/classops.mli
index 5aa8b7aaf8..fbc6c39fbd 100644
--- a/pretyping/classops.mli
+++ b/pretyping/classops.mli
@@ -52,7 +52,8 @@ val class_info_from_index : int -> cl_typ * cl_info_typ
val coercion_exists : coe_typ -> bool
val coercion_info : coe_typ -> (int * coe_info_typ)
val coercion_info_from_index : int -> coe_typ * coe_info_typ
-val coercion_params : reference -> int (* raise Not_found if not a coercion *)
+val coercion_params :
+ reference -> int (* raise [Not_found] if not a coercion *)
val constructor_at_head : constr -> cl_typ * int
val class_of : env -> 'c evar_map -> constr -> constr * int
val class_args_of : constr -> constr list