aboutsummaryrefslogtreecommitdiff
path: root/toplevel/coqloop.ml
diff options
context:
space:
mode:
Diffstat (limited to 'toplevel/coqloop.ml')
-rw-r--r--toplevel/coqloop.ml10
1 files changed, 2 insertions, 8 deletions
diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml
index de2a81b7c9..b27f7ae31a 100644
--- a/toplevel/coqloop.ml
+++ b/toplevel/coqloop.ml
@@ -339,14 +339,8 @@ let feed_emacs = function
let rec loop () =
Sys.catch_break true;
- if !Flags.print_emacs then begin
- (* TODO : check with Enrico ?! *)
- (*
- Pp.set_feeder feed_emacs;
- Vernacentries.enable_goal_printing := false;
- *)
- Vernacentries.qed_display_script := false;
- end;
+ if !Flags.print_emacs then Vernacentries.qed_display_script := false;
+ Flags.coqtop_ui := true;
try
reset_input_buffer stdin top_buffer;
while true do do_vernac(); flush_all() done