From 2aaced1d2486deb901ea0a5b134ef28273dda67f Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 10 Jul 2015 01:17:56 +0200
Subject: 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).
---
 pretyping/classops.mli | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'pretyping/classops.mli')

diff --git a/pretyping/classops.mli b/pretyping/classops.mli
index c421b4505b..e2bb2d1a00 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 ->
-- 
cgit v1.2.3