diff options
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/success/intros.v | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/test-suite/success/intros.v b/test-suite/success/intros.v index 17f160f98e..11156aa0ee 100644 --- a/test-suite/success/intros.v +++ b/test-suite/success/intros.v @@ -78,3 +78,9 @@ intros H2%H%H0. - exact H2. - exact H1. Qed. + +(* Bug found by Enrico *) + +Goal forall x : nat, True. +intros y%(fun x => x). +Abort. |