From 2280477a96e19ba5060de2d48dcc8fd7c8079d22 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <gareuselesinge@debian.org>
Date: Fri, 13 Nov 2015 11:31:34 +0100
Subject: Imported Upstream version 8.5~beta3+dfsg

---
 pretyping/coercion.ml | 28 ++++++++++++++++------------
 1 file changed, 16 insertions(+), 12 deletions(-)

(limited to 'pretyping/coercion.ml')

diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index 8ebb8cd2..e61e52c1 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -295,8 +295,8 @@ and coerce loc env evdref (x : Term.constr) (y : Term.constr)
 		   let evm = !evdref in
 		     (try subco ()
 		      with NoSubtacCoercion ->
-			let typ = Typing.type_of env evm c in
-			let typ' = Typing.type_of env evm c' in
+			let typ = Typing.unsafe_type_of env evm c in
+			let typ' = Typing.unsafe_type_of env evm c' in
 			  (* 			     if not (is_arity env evm typ) then *)
 			  coerce_application typ typ' c c' l l')
 		       (* 			     else subco () *)
@@ -305,8 +305,8 @@ and coerce loc env evdref (x : Term.constr) (y : Term.constr)
 	   | x, y when Constr.equal c c' ->
 	       if Int.equal (Array.length l) (Array.length l') then
 		 let evm =  !evdref in
-		 let lam_type = Typing.type_of env evm c in
-		 let lam_type' = Typing.type_of env evm c' in
+		 let lam_type = Typing.unsafe_type_of env evm c in
+		 let lam_type' = Typing.unsafe_type_of env evm c' in
 		   (* 			 if not (is_arity env evm lam_type) then ( *)
 		   coerce_application lam_type lam_type' c c' l l'
 		     (* 			 ) else subco () *)
@@ -345,7 +345,7 @@ let saturate_evd env evd =
   Typeclasses.resolve_typeclasses
     ~filter:Typeclasses.no_goals ~split:false ~fail:false env evd
 
-(* appliquer le chemin de coercions p à hj *)
+(* Apply coercion path from p to hj; raise NoCoercion if not applicable *)
 let apply_coercion env sigma p hj typ_cl =
   try
     let j,t,evd = 
@@ -367,7 +367,8 @@ let apply_coercion env sigma p hj typ_cl =
   with NoCoercion as e -> raise e
   | e when Errors.noncritical e -> anomaly (Pp.str "apply_coercion")
 
-let inh_app_fun env evd j =
+(* Try to coerce to a funclass; raise NoCoercion if not possible *)
+let inh_app_fun_core env evd j =
   let t = whd_betadeltaiota env evd j.uj_type in
     match kind_of_term t with
     | Prod (_,_,_) -> (evd,j)
@@ -378,7 +379,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,15 +388,17 @@ let inh_app_fun env evd j =
 	      (!evdref, res)
 	  with NoSubtacCoercion | NoCoercion ->
 	    (evd,j)
+          else raise NoCoercion
 
+(* Try to coerce to a funclass; returns [j] if no coercion is applicable *)
 let inh_app_fun resolve_tc env evd j =
-  try inh_app_fun env evd j
+  try inh_app_fun_core env evd j
   with
-  | Not_found when not resolve_tc 
+  | NoCoercion when not resolve_tc
     || not !use_typeclasses_for_conversion -> (evd, j)
-  | Not_found ->
-    try inh_app_fun env (saturate_evd env evd) j
-    with Not_found -> (evd, j)
+  | NoCoercion ->
+    try inh_app_fun_core env (saturate_evd env evd) j
+    with NoCoercion -> (evd, j)
 
 let inh_tosort_force loc env evd j =
   try
-- 
cgit v1.2.3