diff options
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/success/pattern.v | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/test-suite/success/pattern.v b/test-suite/success/pattern.v index 23e6f8e359..72f84052d7 100644 --- a/test-suite/success/pattern.v +++ b/test-suite/success/pattern.v @@ -42,3 +42,8 @@ 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. |