From f9be7230b24be929ba8539932aabcb6a682ea6e2 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 25 Jun 2010 10:09:43 +0000
Subject: Restored a "feature" of unification in pre-8.3 (it was used e.g. in a
 proof of Chung-Kil's Hur Heq package): conversion in "trivial_unify" accepted
 evars as ordinary variables. I hope I did not invalidate some features that
 would have needed restricting conversion on evar-free terms, but since
 failure of conversion in presence of evars is redirected to the main
 unification algorithm, I guess it is OK. For better readibility, I also
 inlined and cleaned a bit trivial_unify.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13193 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 test-suite/success/rewrite.v | 28 ++++++++++++++++++++++++++++
 1 file changed, 28 insertions(+)

(limited to 'test-suite')

diff --git a/test-suite/success/rewrite.v b/test-suite/success/rewrite.v
index 9bc6800724..3bce52fe78 100644
--- a/test-suite/success/rewrite.v
+++ b/test-suite/success/rewrite.v
@@ -80,3 +80,31 @@ Undo.
 intros; inversion H; dependent rewrite <- H4 in H0.
 Abort.
 
+(* Test conversion between terms with evars that both occur in K-redexes and
+   are elsewhere solvable.
+
+   This is quite an artificial example, but it used to work in 8.2.
+
+   Since rewrite supports conversion on terms without metas, it
+   was successively unifying (id 0 ?y) and 0 where ?y was not a
+   meta but, because coming from a "_", an evar.
+
+   After commit r12440 which unified the treatment of metas and
+   evars, it stopped to work. Chung-Kil Hur's Heq package used
+   this feature. Solved in r13...
+*)
+
+Parameter g : nat -> nat -> nat.
+Definition K (x y:nat) := x.
+
+Goal (forall y, g y (K 0 y) = 0) -> g 0 0 = 0.
+intros.
+rewrite (H _).
+reflexivity.
+Qed.
+
+Goal (forall y, g (K 0 y) y = 0) -> g 0 0 = 0.
+intros.
+rewrite (H _).
+reflexivity.
+Qed.
-- 
cgit v1.2.3