diff options
| author |  Stephane Glondu <steph@glondu.net> | 2010-07-21 09:46:51 +0200 |
|---|---|---|
| committer | Stephane Glondu <steph@glondu.net> | 2010-07-21 09:46:51 +0200 |
| commit | 5b7eafd0f00a16d78f99a27f5c7d5a0de77dc7e6 (patch) | |
| tree | 631ad791a7685edafeb1fb2e8faeedc8379318ae /test-suite/success/change.v | |
| parent | da178a880e3ace820b41d38b191d3785b82991f5 (diff) | |
Imported Upstream snapshot 8.3~beta0+13298
Diffstat (limited to 'test-suite/success/change.v')
| -rw-r--r-- | test-suite/success/change.v | 26 |
1 files changed, 26 insertions, 0 deletions
diff --git a/test-suite/success/change.v b/test-suite/success/change.v index cea01712..5ac6ce82 100644 --- a/test-suite/success/change.v +++ b/test-suite/success/change.v @@ -4,3 +4,29 @@ Goal let a := 0+0 in a=a. intro. change 0 in (value of a). change ((fun A:Type => A) nat) in (type of a). +Abort. + +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. + *) |