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 /toplevel | |
| parent | 773d95f915996b581b7ea82d9193197649c951a0 (diff) | |
Adding an option "Printing Unfocused".
Off by default.
+ small refactoring of emacs hacks in printer.ml.
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/coqtop.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index c3a755860..5687418f2 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -247,6 +247,7 @@ let set_emacs () = if not (Option.is_empty !toploop) then error "Flag -emacs is incompatible with a custom toplevel loop"; Flags.print_emacs := true; + Printer.enable_goal_tags_printing := true; color := `OFF (** Options for CoqIDE *) |