From 4944b5e72c0f4bfcf1ae140f810d8666dac3cf60 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 15 May 2015 14:26:35 +0200
Subject: Make Coercion.inh_app_fun respect its specification.

It enhances bug #3527, as instead of raising an anomaly "Uncaught
exception Coercion.NoCoercion(_)", it now fails with a typing error.
---
 pretyping/coercion.ml | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index f5135f5c60..6765ca130b 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -378,7 +378,8 @@ let inh_app_fun env evd j =
       	try let t,p =
 	  lookup_path_to_fun_from env evd j.uj_type in
 	    apply_coercion env evd p j t
-	with Not_found | NoCoercion when Flags.is_program_mode () ->
+	with Not_found | NoCoercion ->
+          if Flags.is_program_mode () then
 	  try
 	    let evdref = ref evd in
 	    let coercef, t = mu env evdref t in
@@ -386,6 +387,7 @@ let inh_app_fun env evd j =
 	      (!evdref, res)
 	  with NoSubtacCoercion | NoCoercion ->
 	    (evd,j)
+          else (evd, j)
 
 let inh_app_fun resolve_tc env evd j =
   try inh_app_fun env evd j
-- 
cgit v1.2.3