From b8b6970da464ebd222f05992f77da641bf98591d Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Wed, 25 Jun 2014 11:41:21 +0200
Subject: Use full transparent state when checking well-typedness of a second
 order matching infered predicate, instead of the arguments ts which might be
 empty (e.g. in unification). Fixes failure in success/unification.v

---
 pretyping/evarconv.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 2761dcbe33..e9d152de2d 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -882,7 +882,8 @@ let second_order_matching ts env_rhs evd (evk,args) argoccs rhs =
       force_instantiation evd !evsref
   | [] ->
     let evd = 
-      try Evarsolve.check_evar_instance evd evk rhs (evar_conv_x ts)
+      try Evarsolve.check_evar_instance evd evk rhs 
+	    (evar_conv_x full_transparent_state)
       with IllTypedInstance _ -> raise (TypingFailed evd)
     in
       Evd.define evk rhs evd 
-- 
cgit v1.2.3