From a3f0a0daf58964a54b1e6fb1f8252f68a8c9c8ea Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Thu, 5 Nov 2015 17:47:39 -0500
Subject: Fix bug #3998: when using typeclass resolution for conversion, allow
 only one disjoint component of the typeclasses instances to resolve.

---
 pretyping/coercion.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index e61e52c178..3163ac0e6e 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -343,7 +343,7 @@ let coerce_itf loc env evd v t c1 =
 
 let saturate_evd env evd =
   Typeclasses.resolve_typeclasses
-    ~filter:Typeclasses.no_goals ~split:false ~fail:false env evd
+    ~filter:Typeclasses.no_goals ~split:true ~fail:false env evd
 
 (* Apply coercion path from p to hj; raise NoCoercion if not applicable *)
 let apply_coercion env sigma p hj typ_cl =
-- 
cgit v1.2.3