Add [Unset Printing Dependent Evars Line]

This allows a work-around for bug #4819,
https://coq.inria.fr/bugs/show_bug.cgi?id=4819.

3 files changed, 41 insertions, 15 deletions

diff --git a/CHANGES b/CHANGES
index 63619a55b..9ef048345 100644
--- a/CHANGES
+++ b/CHANGES
@@ -65,6 +65,9 @@ Tools
 - coqc accepts a -o option to specify the output file name
 - coqtop accepts --print-version to print Coq and OCaml versions in
   easy to parse format
+- Setting [Printing Dependent Evars Line] can be unset to disable the
+  computation associated with printing the "dependent evars: " line in
+  -emacs mode
 
 Changes from V8.5pl1 to V8.5pl2
 ===============================
@@ -507,8 +510,8 @@ Tactics
 - When given a reference as argument, simpl, vm_compute and
   native_compute now strictly interpret it as the head of a pattern
   starting with this reference.
-- The "change p with c" tactic semantics changed, now type-checking 
-  "c" at each matching occurrence "t" of the pattern "p", and 
+- The "change p with c" tactic semantics changed, now type-checking
+  "c" at each matching occurrence "t" of the pattern "p", and
   converting "t" with "c".
 - Now "appcontext" and "context" behave the same. The old buggy behavior of
   "context" can be retrieved at parse time by setting the
diff --git a/doc/refman/RefMan-oth.tex b/doc/refman/RefMan-oth.tex
index aea2bae38..6a8bda35d 100644
--- a/doc/refman/RefMan-oth.tex
+++ b/doc/refman/RefMan-oth.tex
@@ -947,6 +947,14 @@ time of writing this documentation, the default value is 50).
 \subsection[\tt Test Printing Depth.]{\tt Test Printing Depth.\optindex{Printing Depth}}
 This command displays the current nesting depth used for display.
 
+\subsection[\tt Set Printing Dependent Evars Line.]{\tt Set Printing Dependent Evars Line.\optindex{Printing Dependent Evars Line}}
+This command enables the printing of the ``{\tt (dependent evars: \ldots)}''
+line when {\tt -emacs} is passed.
+
+\subsection[\tt Unset Printing Dependent Evars Line.]{\tt Unset Printing Dependent Evars Line.\optindex{Printing Dependent Evars Line}}
+This command disables the printing of the ``{\tt (dependent evars: \ldots)}''
+line when {\tt -emacs} is passed.
+
 %\subsection{\tt Abstraction ...}
 %Not yet documented.
 
diff --git a/printing/printer.ml b/printing/printer.ml
index 8af2af98a..0bac2755b 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -496,6 +496,18 @@ let print_evar_constraints gl sigma cstrs =
   in
   prlist_with_sep fnl pr_evconstr cstrs
 
+let should_print_dependent_evars = ref true
+
+let _ =
+  let open Goptions in
+  declare_bool_option
+    { optsync  = true;
+      optdepr  = false;
+      optname  = "Printing Dependent Evars Line";
+      optkey   = ["Printing";"Dependent";"Evars";"Line"];
+      optread  = (fun () -> !should_print_dependent_evars);
+      optwrite = (fun v -> should_print_dependent_evars := v) }
+
 let print_dependent_evars gl sigma seeds =
   let constraints =
     let _, cstrs = Evd.extract_all_conv_pbs sigma in
@@ -504,21 +516,25 @@ let print_dependent_evars gl sigma seeds =
          ++ str":" ++ fnl () ++ hov 0 (print_evar_constraints gl sigma cstrs)
   in
   let evars () =
-    let evars = Evarutil.gather_dependent_evars sigma seeds in
-    let evars =
-      Evar.Map.fold begin fun e i s ->
-	let e' = pr_internal_existential_key e in
-	match i with
-	| None -> s ++ str" " ++ e' ++ str " open,"
-	| Some i ->
-	  s ++ str " " ++ e' ++ str " using " ++
-	    Evar.Set.fold begin fun d s ->
-	      pr_internal_existential_key d ++ str " " ++ s
-	    end i (str ",")
-      end evars (str "")
+    if !should_print_dependent_evars then
+      let evars = Evarutil.gather_dependent_evars sigma seeds in
+      let evars =
+	Evar.Map.fold begin fun e i s ->
+	  let e' = pr_internal_existential_key e in
+	  match i with
+	  | None -> s ++ str" " ++ e' ++ str " open,"
+	  | Some i ->
+	    s ++ str " " ++ e' ++ str " using " ++
+	      Evar.Set.fold begin fun d s ->
+		pr_internal_existential_key d ++ str " " ++ s
+	      end i (str ",")
+	end evars (str "")
     in
     fnl () ++
     str "(dependent evars:" ++ evars ++ str ")" ++ fnl ()
+    else
+      fnl () ++
+	str "(dependent evars: (printing disabled) )" ++ fnl ()
   in
   constraints ++ delayed_emacs_cmd evars
 
@@ -869,4 +885,3 @@ let pr_polymorphic b =
 let pr_universe_instance evd ctx =
   let inst = Univ.UContext.instance ctx in
     str"@{" ++ Univ.Instance.pr (Evd.pr_evd_level evd) inst ++ str"}"
-