diff options
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/success/intros.v | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/test-suite/success/intros.v b/test-suite/success/intros.v index bb9fc0c50d..9443d01e3b 100644 --- a/test-suite/success/intros.v +++ b/test-suite/success/intros.v @@ -28,3 +28,8 @@ Goal forall n p, n + p = 0. intros [|*]; intro p. Abort. +(* Check non-interference of "_" with name generation *) +Goal True -> True -> True. +intros _ ?. +exact H. +Qed. |