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.

1 files changed, 6 insertions, 1 deletions

diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml
index efcde3d1b..2c6e7e736 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 =