From ddc4d94e9fc45f1aa058c52bba8d914048592153 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Wed, 27 Aug 2014 17:43:13 +0200
Subject: Protect against "it's unifiable, if you solve some unsolvable
 constraints" behavior of evar_conv_x, getting more common after patch on
 evars and eta. The main problem is that ?X = C[?X] problems get postponed
 now, when they failed earlier before (rendering the algorithm incomplete,
 e.g. on ?X = \y. ?X y). A notion of "rigid/strongly rigid" occurrences would
 give a better fix.

---
 tactics/rewrite.ml | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml
index efcde3d1be..2c6e7e736a 100644
--- a/tactics/rewrite.ml
+++ b/tactics/rewrite.ml
@@ -443,7 +443,12 @@ let split_head = function
   | [] -> assert(false)
 
 let evd_convertible env evd x y =
-  try ignore(Evarconv.the_conv_x env x y evd); true
+  try let evd = Evarconv.the_conv_x env x y evd in 
+      (* Unfortunately, the_conv_x might say they are unifiable even if some
+	 unsolvable constraints remain, so we check them here *)
+      let evd = Evarconv.consider_remaining_unif_problems env evd in
+	Evarconv.check_problems_are_solved env evd;
+	true
   with e when Errors.noncritical e -> false
 
 let convertible env evd x y =
-- 
cgit v1.2.3