summaryrefslogtreecommitdiff
path: root/pretyping/classops.mli
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping/classops.mli')
-rw-r--r--pretyping/classops.mli4
1 files changed, 2 insertions, 2 deletions
diff --git a/pretyping/classops.mli b/pretyping/classops.mli
index c421b450..e2bb2d1a 100644
--- a/pretyping/classops.mli
+++ b/pretyping/classops.mli
@@ -78,9 +78,9 @@ val coercion_value : coe_index -> (unsafe_judgment * bool * bool) Univ.in_univer
(** {6 Lookup functions for coercion paths } *)
-val lookup_path_between_class : cl_index * cl_index -> inheritance_path
-(** @raise Not_found when no such path exists *)
+(** @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 : env -> evar_map -> types * types ->
types * types * inheritance_path
val lookup_path_to_fun_from : env -> evar_map -> types ->