diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-12-30 12:02:32 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-12-30 12:02:32 +0000 |
| commit | 306d1be283442c361aa26d000d339f3f4dfbeab9 (patch) | |
| tree | 5fdec06c70ef551f8b775988820fb07c7538e29f /test-suite/success/change.v | |
| parent | 77d86619f5f557de52a391f6811bacd73c01580b (diff) | |
Fixing bug #2146 (broken selection of occurrences in "change").
In trunk the different possible combinations of "at" and "in" with
occurrences are taken into account.
In 8.2 branch, it remains fragile (syntaxes that were accepted remain
accepted and a message warns if the occurrences coming after the
"with" are not taken into account).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12614 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'test-suite/success/change.v')
| -rw-r--r-- | test-suite/success/change.v | 20 |
1 files changed, 20 insertions, 0 deletions
diff --git a/test-suite/success/change.v b/test-suite/success/change.v index c72ee875a..5ac6ce82b 100644 --- a/test-suite/success/change.v +++ b/test-suite/success/change.v @@ -10,3 +10,23 @@ Goal forall x, 2 + S x = 1 + S x. intro. change (?u + S x) with (S (u + x)). Abort. + +(* Check the combination of at, with and in (see bug #2146) *) + +Goal 3=3 -> 3=3. intro H. +change 3 at 2 with (1+2) in |- *. +change 3 at 2 with (1+2) in H |-. +change 3 with (1+2) in H at 1 |- * at 1. +(* Now check that there are no more 3's *) +change 3 with (1+2) in * || reflexivity. +Qed. + +(* Note: the following is invalid and must fail +change 3 at 1 with (1+2) at 3. +change 3 at 1 with (1+2) in *. +change 3 at 1 with (1+2) in H at 2 |-. +change 3 at 1 with (1+2) in |- * at 3. +change 3 at 1 with (1+2) in H |- *. +change 3 at 1 with (1+2) in H, H|-. +change 3 in |- * at 1. + *) |