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