From e6bf1b6936f8bd61eb1266f7f4dd67181f3630f1 Mon Sep 17 00:00:00 2001
From: msozeau
Date: Wed, 11 Jul 2012 16:03:41 +0000
Subject: Fix regression introduced in r15418 that broke MathClasses. In
 program mode, try program coercions before the last resort typeclass
 resolution to resolve a conversion problem.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15595 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 pretyping/coercion.ml | 24 +++++++++++-------------
 1 file changed, 11 insertions(+), 13 deletions(-)

diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index 524d9d058e..7fd4d1cc29 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -319,11 +319,9 @@ let coerce_itf loc env isevars v t c1 =
   let t = Option.map (app_opt env evars coercion) v in
     !evars, t
 
-
-
 let saturate_evd env evd =
   Typeclasses.resolve_typeclasses
-    ~filter:Typeclasses.no_goals ~split:true ~fail:false env evd
+    ~filter:Typeclasses.no_goals ~split:false ~fail:false env evd
 
 (* appliquer le chemin de coercions p à hj *)
 let apply_coercion env sigma p hj typ_cl =
@@ -461,16 +459,16 @@ let inh_conv_coerce_to_gen rigidonly loc env evd cj t =
     try
       inh_conv_coerce_to_fail loc env evd rigidonly (Some cj.uj_val) cj.uj_type t
     with NoCoercion ->
-      let evd = saturate_evd env evd in
-	try
-	  inh_conv_coerce_to_fail loc env evd rigidonly (Some cj.uj_val) cj.uj_type t
-	with NoCoercion ->
-	  (if Flags.is_program_mode () then
-	     try
-	       coerce_itf loc env evd (Some cj.uj_val) cj.uj_type t
-	     with NoSubtacCoercion ->
-	       error_actual_type_loc loc env evd cj t
-	   else error_actual_type_loc loc env evd cj t)
+      try
+	if Flags.is_program_mode () then
+	  coerce_itf loc env evd (Some cj.uj_val) cj.uj_type t
+	else raise NoSubtacCoercion
+      with NoSubtacCoercion ->
+	let evd = saturate_evd env evd in
+      	  try
+      	    inh_conv_coerce_to_fail loc env evd rigidonly (Some cj.uj_val) cj.uj_type t
+      	  with NoCoercion ->
+	    error_actual_type_loc loc env evd cj t
   in
   let val' = match val' with Some v -> v | None -> assert(false) in
     (evd',{ uj_val = val'; uj_type = t })
-- 
cgit v1.2.3