[glob/aux files] Remove undocumented Stdout dump, cleanup flags.

Fixes #10640

We remove the `StdOut` dump target, so now dump will only happen if a
file is specified. Indeed, we make the default no to dump, and enable
dump only in coqc, moving the option to the `Coqcargs` module.

No need for a changes entry as this feature was undocumented, and no
use case was given when introduced.

Output to feedback must be explicitly enabled by clients / coqidetop,
and we have thus also removed the undocumented option `-feedback-glob`.

2 files changed, 18 insertions, 28 deletions

diff --git a/interp/dumpglob.ml b/interp/dumpglob.ml
index 8d6a266c30..41d1da9694 100644
--- a/interp/dumpglob.ml
+++ b/interp/dumpglob.ml
@@ -20,31 +20,21 @@ let open_glob_file f =
 let close_glob_file () =
   close_out !glob_file
 
-type glob_output_t =
-    | NoGlob
-    | StdOut
-    | MultFiles
-    | Feedback
-    | File of string
+type glob_output =
+  | NoGlob
+  | Feedback
+  | MultFiles
+  | File of string
 
 let glob_output = ref NoGlob
 
-let dump () = !glob_output != NoGlob
+let dump () = !glob_output <> NoGlob
 
-let noglob () = glob_output := NoGlob
-
-let dump_to_dotglob () = glob_output := MultFiles
-
-let dump_into_file f =
-  if String.equal f "stdout" then
-    (glob_output := StdOut; glob_file := stdout)
-  else
-    (glob_output := File f; open_glob_file f)
-
-let feedback_glob () = glob_output := Feedback
+let set_glob_output mode =
+  glob_output := mode
 
 let dump_string s =
-  if dump () && !glob_output != Feedback then 
+  if dump () && !glob_output != Feedback then
     output_string !glob_file s
 
 let start_dump_glob ~vfile ~vofile =
@@ -57,13 +47,13 @@ let start_dump_glob ~vfile ~vofile =
   | File f ->
       open_glob_file f;
       output_string !glob_file "DIGEST NO\n"
-  | NoGlob | Feedback | StdOut ->
+  | NoGlob | Feedback ->
       ()
 
 let end_dump_glob () =
   match !glob_output with
   | MultFiles | File _ -> close_glob_file ()
-  | NoGlob | Feedback | StdOut -> ()
+  | NoGlob | Feedback -> ()
 
 let previous_state = ref MultFiles
 let pause () = previous_state := !glob_output; glob_output := NoGlob
diff --git a/interp/dumpglob.mli b/interp/dumpglob.mli
index 60d62a1cb2..2b6a116a01 100644
--- a/interp/dumpglob.mli
+++ b/interp/dumpglob.mli
@@ -8,19 +8,19 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-val open_glob_file : string -> unit
-val close_glob_file : unit -> unit
-
 val start_dump_glob : vfile:string -> vofile:string -> unit
 val end_dump_glob : unit -> unit
 
 val dump : unit -> bool
 
-val noglob : unit -> unit
-val dump_into_file : string -> unit (** special handling of "stdout" *)
+type glob_output =
+  | NoGlob
+  | Feedback
+  | MultFiles                   (* one glob file per .v file *)
+  | File of string              (* Single file for all coqc arguments *)
 
-val dump_to_dotglob : unit -> unit
-val feedback_glob : unit -> unit
+(* Default "NoGlob" *)
+val set_glob_output : glob_output -> unit
 
 val pause : unit -> unit
 val continue : unit -> unit