diff options
| -rw-r--r-- | test-suite/success/apply.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/test-suite/success/apply.v b/test-suite/success/apply.v index 30fa4129d7..454a118d61 100644 --- a/test-suite/success/apply.v +++ b/test-suite/success/apply.v @@ -16,7 +16,7 @@ Qed. (* Check if it unfolds when there are not enough premises *) Goal forall n, n = S n -> False. -intro. +intros. apply n_Sn in H. assumption. Qed. |