diff options
| author |  Pierre Courtieu <Pierre.Courtieu@cnam.fr> | 2017-04-26 11:57:58 +0200 |
|---|---|---|
| committer | Pierre Courtieu <Pierre.Courtieu@cnam.fr> | 2017-05-04 11:13:49 +0200 |
| commit | 1fe73e6af81759fa8b78c8660745492ed886d477 (patch) | |
| tree | 4847f56a199aa1f2cd433b3f0c1d791563634fbe /ide/coqide_ui.ml | |
| parent | 773d95f915996b581b7ea82d9193197649c951a0 (diff) | |
Adding an option "Printing Unfocused".
Off by default.
+ small refactoring of emacs hacks in printer.ml.
Diffstat (limited to 'ide/coqide_ui.ml')
| -rw-r--r-- | ide/coqide_ui.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/ide/coqide_ui.ml b/ide/coqide_ui.ml index 91c281c8d..717c4000f 100644 --- a/ide/coqide_ui.ml +++ b/ide/coqide_ui.ml @@ -85,6 +85,7 @@ let init () = \n <menuitem action='Display existential variable instances' />\ \n <menuitem action='Display universe levels' />\ \n <menuitem action='Display all low-level contents' />\ +\n <menuitem action='Display unfocused goals' />\ \n </menu>\ \n <menu action='Navigation'>\ \n <menuitem action='Forward' />\ |