summaryrefslogtreecommitdiff
path: root/pretyping/classops.mli
diff options
context:
space:
mode:
authorGravatar Enrico Tassi <gareuselesinge@debian.org>2015-11-13 11:43:34 +0100
committerGravatar Enrico Tassi <gareuselesinge@debian.org>2015-11-13 11:43:34 +0100
commit4e76c4f01b69b77f40686e06c4544aa156efaa5a (patch)
treeaefad2e3de35f75c46729f9310d33b56d3821961 /pretyping/classops.mli
parent64fa31c7ee53e79b112507fb2eea27dc7648328d (diff)
parent91dbeab8eef959c3f64960909ca69d4e68c8198d (diff)
Imported Upstream version 8.5~beta3+dfsg
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 ->