From 61f4df8b5b974302e8b48bcf271aa68757db69fe Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Thu, 8 Aug 2019 23:15:19 +0200
Subject: [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`.
---
 tactics/declare.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'tactics')

diff --git a/tactics/declare.ml b/tactics/declare.ml
index c280760e84..c23ee4a76e 100644
--- a/tactics/declare.ml
+++ b/tactics/declare.ml
@@ -224,7 +224,7 @@ let cast_opaque_proof_entry e =
         let vars = global_vars_set env pf in
         ids_typ, vars
     in
-    let () = if !Flags.record_aux_file then record_aux env hyp_typ hyp_def in
+    let () = if Aux_file.recording () then record_aux env hyp_typ hyp_def in
     keep_hyps env (Id.Set.union hyp_typ hyp_def)
   | Some hyps -> hyps
   in
-- 
cgit v1.2.3