From 1fe73e6af81759fa8b78c8660745492ed886d477 Mon Sep 17 00:00:00 2001
From: Pierre Courtieu <Pierre.Courtieu@cnam.fr>
Date: Wed, 26 Apr 2017 11:57:58 +0200
Subject: Adding an option "Printing Unfocused".

Off by default.

+ small refactoring of emacs hacks in printer.ml.
---
 toplevel/coqtop.ml | 1 +
 1 file changed, 1 insertion(+)

(limited to 'toplevel')

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 *)
-- 
cgit v1.2.3