diff options
author | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-06-25 10:09:43 +0000 |
---|---|---|
committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-06-25 10:09:43 +0000 |
commit | f9be7230b24be929ba8539932aabcb6a682ea6e2 (patch) | |
tree | 41e047edf48b9dccda5e79d8108dcafb56cbd1ab /test-suite | |
parent | 68da8bd15b9e8d7bfae0baa21195d6f1e6b93311 (diff) |
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
Diffstat (limited to 'test-suite')
-rw-r--r-- | test-suite/success/rewrite.v | 28 |
1 files changed, 28 insertions, 0 deletions
diff --git a/test-suite/success/rewrite.v b/test-suite/success/rewrite.v index 9bc680072..3bce52fe7 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. |