diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-07-10 01:17:56 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-07-10 19:18:41 +0200 |
| commit | 2aaced1d2486deb901ea0a5b134ef28273dda67f (patch) | |
| tree | d5d7cccb1fc0b6d9132e1f5fcdc0d1a8b3afb7ff /pretyping/classops.mli | |
| parent | 9c732a5c878bac2592cb397aca3d17cfefdcd023 (diff) | |
Continuing handling of NoCoercion after df6e64fd28 and 4944b5e72.
Commit df6e64fd28 let apply_coercion raise NoCoercion untrapped by inh_app_fun.
Commit 4944b5e72 caught NoCoercion but missed re-attempting inserting a
coercion after resolving instances of type classes.
This fixes MathClasses (while preserving fix of part of from 4944b5e72
and fixes of HoTT_coq_014.v from df6e64fd28).
Diffstat (limited to 'pretyping/classops.mli')
| -rw-r--r-- | pretyping/classops.mli | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/pretyping/classops.mli b/pretyping/classops.mli index c421b4505..e2bb2d1a0 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 -> |