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/pattern.v | |
parent | da178a880e3ace820b41d38b191d3785b82991f5 (diff) |
Imported Upstream snapshot 8.3~beta0+13298
Diffstat (limited to 'test-suite/success/pattern.v')
-rw-r--r-- | test-suite/success/pattern.v | 42 |
1 files changed, 42 insertions, 0 deletions
diff --git a/test-suite/success/pattern.v b/test-suite/success/pattern.v index 28d0bd55..72f84052 100644 --- a/test-suite/success/pattern.v +++ b/test-suite/success/pattern.v @@ -5,3 +5,45 @@ Goal (id true,id false)=(id true,id true). generalize bool at 2 4 6 8 10 as B, true at 3 as tt, false as ff. +Abort. + +(* Check use of occurrences in hypotheses for a reduction tactic such + as pattern *) + +(* Did not work in 8.2 *) +Goal 0=0->True. +intro H. +pattern 0 in H at 2. +set (f n := 0 = n) in H. (* check pattern worked correctly *) +Abort. + +(* Syntactic variant which was working in 8.2 *) +Goal 0=0->True. +intro H. +pattern 0 at 2 in H. +set (f n := 0 = n) in H. (* check pattern worked correctly *) +Abort. + +(* Ambiguous occurrence selection *) +Goal 0=0->True. +intro H. +pattern 0 at 1 in H at 2 || exact I. (* check pattern fails *) +Qed. + +(* Ambiguous occurrence selection *) +Goal 0=1->True. +intro H. +pattern 0, 1 in H at 1 2 || exact I. (* check pattern fails *) +Qed. + +(* Occurrence selection shared over hypotheses is difficult to advocate and + hence no longer allowed *) +Goal 0=1->1=0->True. +intros H1 H2. +pattern 0 at 1, 1 in H1, H2 || exact I. (* check pattern fails *) +Qed. + +(* Test catching of reduction tactics errors (was not the case in 8.2) *) +Goal eq_refl 0 = eq_refl 0. +pattern 0 at 1 || reflexivity. +Qed. |