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 /ide/tags.mli | |
| 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 'ide/tags.mli')
| -rw-r--r-- | ide/tags.mli | 3 |
1 files changed, 0 insertions, 3 deletions
diff --git a/ide/tags.mli b/ide/tags.mli index e68015c99..14cfd0dbf 100644 --- a/ide/tags.mli +++ b/ide/tags.mli @@ -21,9 +21,6 @@ sig val tooltip : GText.tag val edit_zone : GText.tag (* for debugging *) val all : GText.tag list - - (* Not part of the all list. Special tags! *) - val read_only : GText.tag end module Proof : |