diff options
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 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. |