diff options
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/ide/undo.v | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/test-suite/ide/undo.v b/test-suite/ide/undo.v index a76817a876..d50f545da1 100644 --- a/test-suite/ide/undo.v +++ b/test-suite/ide/undo.v @@ -72,3 +72,8 @@ Definition p := O. assert True by trivial. trivial. Qed. + +(* Undoing declarations, not in proof *) + +Definition q := O. +Definition r := O. |