diff options
Diffstat (limited to 'test-suite/success')
| -rw-r--r-- | test-suite/success/change.v | 11 |
1 files changed, 8 insertions, 3 deletions
diff --git a/test-suite/success/change.v b/test-suite/success/change.v index 5a8f735151..2f676cf9ad 100644 --- a/test-suite/success/change.v +++ b/test-suite/success/change.v @@ -71,8 +71,13 @@ Qed. (* Mini-check that no_check does not check *) -Goal False. -change_no_check True. -exact I. +Goal True -> False. +intro H. +change_no_check nat. +apply S. +change_no_check nat with bool. +change_no_check nat in H. +change_no_check nat with (bool->bool) in H. +exact (H true). Fail Qed. Abort. |