diff options
| author |  Enrico Tassi <Enrico.Tassi@inria.fr> | 2015-04-02 15:47:52 +0200 |
|---|---|---|
| committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2015-04-02 15:57:45 +0200 |
| commit | 20457cbff0b851ac9099847c91f74d48c5fe5be6 (patch) | |
| tree | 6e3277c4fa6148303f6596e320b42bb94068722b /doc/stdlib | |
| parent | fe87c2cab20335b2d5dff61054700597e515f8a1 (diff) | |
CoqIDE: simpler way of reopening/reclosing a proof (Close: 4168)
No "read-only" terminator. If no terminator is present the UI
complains. If the terminator is different, STM warns but
continues. The STM warns that the "check the document" button
will not honor the terminator change, and what to do to avoid
that.
Technically, one cannot turn (a posteriori) an axiom into a theorem
and vice versa. Could be done, but not with a small patch.
Diffstat (limited to 'doc/stdlib')
0 files changed, 0 insertions, 0 deletions