From 6b041a242607ec906fbab451e53c15af6339e4ef Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Thu, 18 May 2017 07:31:36 +0200 Subject: [emacs] [toplevel] Make emacs flag local to the toplevel. We remove the emacs-specific printing code from the core of Coq, now `-emacs` is a printing flag controlled by the toplevel. --- printing/printer.ml | 6 ------ 1 file changed, 6 deletions(-) (limited to 'printing/printer.ml') diff --git a/printing/printer.ml b/printing/printer.ml index ebe68680f..3c31dd96b 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -26,9 +26,6 @@ module RelDecl = Context.Rel.Declaration module NamedDecl = Context.Named.Declaration module CompactedDecl = Context.Compacted.Declaration -let emacs_str s = - if !Flags.print_emacs then s else "" - let get_current_context () = Pfedit.get_current_context () @@ -656,9 +653,6 @@ let print_dependent_evars gl sigma seeds = in cut () ++ cut () ++ str "(dependent evars:" ++ evars ++ str ")" - else if !Flags.print_emacs then - (* IDEs prefer something dummy instead of nothing *) - cut () ++ cut () ++ str "(dependent evars: (printing disabled) )" else mt () in constraints ++ evars () -- cgit v1.2.3