diff options
| author | Emilio Jesus Gallego Arias | 2019-02-12 00:49:56 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-03-27 23:56:18 +0100 |
| commit | e18c553a4ab27ecabebd968fe4f2fdd18ea19101 (patch) | |
| tree | d2045ba4963a8c7e02817eb95dee35b579a0f664 /dev | |
| parent | 43f3634a0e75381ca473aea08415e3d262e4c066 (diff) | |
[vernacular] Make `Show` fail again when no goals remain.
This is used in the test-suite to check that a proof is closed; I am
not sure we'd like to keep this patch tho: the non-failing semantics
seems saner for IDEs.
[main users are in `test-suite/ide`]
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions