[flags] Flag `open Flags`

An incoming commit is removing some toplevel-specific global flags in
favor of local toplevel state; this commit flags `Flags` use so it
becomes clearer in the code whether we are relying on some "global"
settable status in code.

A good candidate for further cleanup is the pattern:

`Flags.if_verbose Feedback.msg_info`

9 files changed, 49 insertions, 58 deletions

diff --git a/checker/checker.ml b/checker/checker.ml
index 7a69700d2..67b812133 100644
--- a/checker/checker.ml
+++ b/checker/checker.ml
@@ -10,7 +10,6 @@ open Pp
 open CErrors
 open Util
 open System
-open Flags
 open Names
 open Check
 
@@ -74,7 +73,7 @@ let add_path ~unix_path:dir ~coq_root:coq_dirpath =
 let convert_string d =
   try Id.of_string d
   with CErrors.UserError _ ->
-    if_verbose Feedback.msg_warning
+    Flags.if_verbose Feedback.msg_warning
       (str "Directory " ++ str d ++ str " cannot be used as a Coq identifier (skipped)");
     raise Exit
 
@@ -342,7 +341,7 @@ let parse_args argv =
     | ("-?"|"-h"|"-H"|"-help"|"--help") :: _ -> usage ()
 
     | ("-v"|"--version") :: _ -> version ()
-    | "-boot" :: rem -> boot := true; parse rem
+    | "-boot" :: rem -> Flags.boot := true; parse rem
     | ("-m" | "--memory") :: rem -> Check_stat.memory_stat := true; parse rem
     | ("-o" | "--output-context") :: rem ->
         Check_stat.output_context := true; parse rem
@@ -374,7 +373,7 @@ let init_with_argv argv =
       parse_args argv;
       if !Flags.debug then Printexc.record_backtrace true;
       Envars.set_coqlib ~fail:(fun x -> CErrors.user_err Pp.(str x));
-      if_verbose print_header ();
+      Flags.if_verbose print_header ();
       init_load_path ();
       engage ();
     with e ->
diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index 1cc072a2a..260cd0444 100644
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
@@ -9,7 +9,6 @@
 open CErrors
 open Util
 open Pp
-open Flags
 open Names
 open Libnames
 open Globnames
@@ -387,7 +386,7 @@ let add_coercion_in_graph (ic,source,target) =
       old_inheritance_graph
   end;
   let is_ambig = match !ambig_paths with [] -> false | _ -> true in
-  if is_ambig && not !quiet then
+  if is_ambig && not !Flags.quiet then
     Feedback.msg_info (message_ambig !ambig_paths)
 
 type coercion = {
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 0f8524e92..57902cb27 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -8,7 +8,6 @@
 
 open Pp
 open CErrors
-open Flags
 open Libnames
 open Coqinit
 
@@ -31,7 +30,7 @@ let print_header () =
   Feedback.msg_notice (str "Welcome to Coq " ++ str ver ++ str " (" ++ str rev ++ str ")");
   flush_all ()
 
-let warning s = with_option Flags.warn Feedback.msg_warning (strbrk s)
+let warning s = Flags.(with_option warn Feedback.msg_warning (strbrk s))
 
 let toploop = ref None
 
@@ -87,7 +86,7 @@ let console_toploop_run () =
   (* We initialize the console only if we run the toploop_run *)
   let tl_feed = Feedback.add_feeder Coqloop.coqloop_feed in
   if Dumpglob.dump () then begin
-    if_verbose warning "Dumpglob cannot be used in interactive mode.";
+    Flags.if_verbose warning "Dumpglob cannot be used in interactive mode.";
     Dumpglob.noglob ()
   end;
   Coqloop.loop();
@@ -130,7 +129,7 @@ let set_type_in_type () =
 let engage () =
   Global.set_engagement !impredicative_set
 
-let set_batch_mode () = batch_mode := true
+let set_batch_mode () = Flags.batch_mode := true
 
 let toplevel_default_name = Names.(DirPath.make [Id.of_string "Top"])
 let toplevel_name = ref toplevel_default_name
@@ -177,7 +176,7 @@ let load_vernacular sid =
     (fun sid (s,v) ->
       let s = Loadpath.locate_file s in
       if !Flags.beautify then
-	with_option beautify_file (Vernac.load_vernac v sid) s
+	Flags.(with_option beautify_file (Vernac.load_vernac v sid) s)
       else
 	Vernac.load_vernac v sid s)
     sid (List.rev !load_vernacular_list)
@@ -199,7 +198,7 @@ let require_prelude () =
 let require_list = ref ([] : string list)
 let add_require s = require_list := s :: !require_list
 let require () =
-  let () = if !load_init then silently require_prelude () in
+  let () = if !Flags.load_init then Flags.silently require_prelude () in
   let map dir = Qualid (Loc.tag @@ qualid_of_string dir) in
   Vernacentries.vernac_require None (Some false) (List.rev_map map !require_list)
 
@@ -229,7 +228,7 @@ let add_compile verbose s =
 
 let compile_file (v,f) =
   if !Flags.beautify then
-    with_option beautify_file (Vernac.compile v) f
+    Flags.(with_option beautify_file (Vernac.compile v) f)
   else
     Vernac.compile v f
 
@@ -304,7 +303,7 @@ let usage () =
   init_load_path ();
   with NoCoqLib -> usage_no_coqlib ()
   end;
-  if !batch_mode then Usage.print_usage_coqc ()
+  if !Flags.batch_mode then Usage.print_usage_coqc ()
   else begin
     Mltop.load_ml_objects_raw_rex
       (Str.regexp (if Mltop.is_native then "^.*top.cmxs$" else "^.*top.cma$"));
@@ -538,7 +537,7 @@ let parse_args arglist =
     |"-with-geoproof" -> Coq_config.with_geoproof := get_bool opt (next ())
     |"-main-channel" -> Spawned.main_channel := get_host_port opt (next())
     |"-control-channel" -> Spawned.control_channel := get_host_port opt (next())
-    |"-vio2vo" -> add_compile false (next ()); Flags.compilation_mode := Vio2Vo
+    |"-vio2vo" -> add_compile false (next ()); Flags.compilation_mode := Flags.Vio2Vo
     |"-toploop" -> set_toploop (next ())
     |"-w" | "-W" -> CWarnings.set_flags (CWarnings.normalize_flags_string (next ()))
     |"-o" -> Flags.compilation_output_name := Some (next())
@@ -551,9 +550,9 @@ let parse_args arglist =
     |"-async-proofs-never-reopen-branch" ->
         Flags.async_proofs_never_reopen_branch := true;
     |"-batch" -> set_batch_mode ()
-    |"-test-mode" -> test_mode := true
-    |"-beautify" -> beautify := true
-    |"-boot" -> boot := true; no_load_rc ()
+    |"-test-mode" -> Flags.test_mode := true
+    |"-beautify" -> Flags.beautify := true
+    |"-boot" -> Flags.boot := true; no_load_rc ()
     |"-bt" -> Backtrace.record_backtrace true
     |"-color" -> set_color (next ())
     |"-config"|"--config" -> print_config := true
@@ -567,17 +566,17 @@ let parse_args arglist =
     |"-indices-matter" -> Indtypes.enforce_indices_matter ()
     |"-just-parsing" -> warning "-just-parsing option has been removed in 8.6"
     |"-m"|"--memory" -> memory_stat := true
-    |"-noinit"|"-nois" -> load_init := false
+    |"-noinit"|"-nois" -> Flags.load_init := false
     |"-no-glob"|"-noglob" -> Dumpglob.noglob (); glob_opt := true
     |"-native-compiler" ->
       if Coq_config.no_native_compiler then
 	warning "Native compilation was disabled at configure time."
-      else native_compiler := true
+      else Flags.native_compiler := true
     |"-output-context" -> output_context := true
     |"-profile-ltac" -> Flags.profile_ltac := true
     |"-q" -> no_load_rc ()
     |"-quiet"|"-silent" -> Flags.quiet := true; Flags.make_warn false
-    |"-quick" -> Flags.compilation_mode := BuildVio
+    |"-quick" -> Flags.compilation_mode := Flags.BuildVio
     |"-list-tags" -> print_tags := true
     |"-time" -> Flags.time := true
     |"-type-in-type" -> set_type_in_type ()
@@ -620,11 +619,11 @@ let init_toplevel arglist =
         prerr_endline "See -help for the list of supported options";
         exit 1
       end;
-      if_verbose print_header ();
+      Flags.if_verbose print_header ();
       inputstate ();
       Mltop.init_known_plugins ();
       engage ();
-      if (not !batch_mode || CList.is_empty !compile_list)
+      if (not !Flags.batch_mode || CList.is_empty !compile_list)
          && Global.env_is_initial ()
       then Declaremods.start_library !toplevel_name;
       init_library_roots ();
@@ -645,16 +644,16 @@ let init_toplevel arglist =
     with any ->
       flush_all();
       let extra =
-        if !batch_mode && not Stateid.(equal (Stm.get_current_state ()) dummy)
+        if !Flags.batch_mode && not Stateid.(equal (Stm.get_current_state ()) dummy)
         then None
         else Some (str "Error during initialization: ")
       in
       fatal_error ?extra any
   end;
-  if !batch_mode then begin
+  if !Flags.batch_mode then begin
     flush_all();
     if !output_context then
-      Feedback.msg_notice (with_option raw_print Prettyp.print_full_pure_context () ++ fnl ());
+      Feedback.msg_notice Flags.(with_option raw_print Prettyp.print_full_pure_context () ++ fnl ());
     Profile.print_profile ();
     exit 0
   end;
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index 1602f9c68..c33f6b9b8 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -11,7 +11,6 @@
 open Pp
 open CErrors
 open Util
-open Flags
 open Vernacexpr
 open Vernacprop
 
@@ -53,7 +52,7 @@ let set_formatter_translator ch =
 
 let pr_new_syntax_in_context ?loc chan_beautify ocom =
   let loc = Option.cata Loc.unloc (0,0) loc in
-  if !beautify_file then set_formatter_translator chan_beautify;
+  if !Flags.beautify_file then set_formatter_translator chan_beautify;
   let fs = States.freeze ~marshallable:`No in
   (* The content of this is not supposed to fail, but if ever *)
   try
@@ -63,7 +62,7 @@ let pr_new_syntax_in_context ?loc chan_beautify ocom =
       | Some com -> Ppvernac.pr_vernac com
       | None -> mt() in
     let after = comment (CLexer.extract_comments (snd loc)) in
-    if !beautify_file then
+    if !Flags.beautify_file then
       (Pp.pp_with !Topfmt.std_ft (hov 0 (before ++ com ++ after));
        Format.pp_print_flush !Topfmt.std_ft ())
     else
@@ -209,7 +208,7 @@ and load_vernac verbosely sid file =
        *)
       in
       (* Printing of vernacs *)
-      if !beautify then pr_new_syntax ?loc in_pa chan_beautify (Some ast);
+      if !Flags.beautify then pr_new_syntax ?loc in_pa chan_beautify (Some ast);
       Option.iter (vernac_echo ?loc) in_echo;
 
       checknav_simple (loc, ast);
@@ -224,7 +223,7 @@ and load_vernac verbosely sid file =
     match e with
       | Stm.End_of_input ->
           (* Is this called so comments at EOF are printed? *)
-          if !beautify then
+          if !Flags.beautify then
             pr_new_syntax ~loc:(Loc.make_loc (max_int,max_int)) in_pa chan_beautify None;
           if !Flags.beautify_file then close_out chan_beautify;
           !rsid
@@ -290,7 +289,7 @@ let compile verbosely f =
                     ++ str ".")
   in
   match !Flags.compilation_mode with
-  | BuildVo ->
+  | Flags.BuildVo ->
       let long_f_dot_v = ensure_v f in
       ensure_exists long_f_dot_v;
       let long_f_dot_vo =
@@ -314,7 +313,7 @@ let compile verbosely f =
         (Printf.sprintf "%.3f" (wall_clock2 -. wall_clock1));
       Aux_file.stop_aux_file ();
       Dumpglob.end_dump_glob ()
-  | BuildVio ->
+  | Flags.BuildVio ->
       let long_f_dot_v = ensure_v f in
       ensure_exists long_f_dot_v;
       let long_f_dot_vio =
@@ -329,7 +328,7 @@ let compile verbosely f =
       check_pending_proofs ();
       Stm.snapshot_vio ldir long_f_dot_vio;
       Stm.reset_task_queue ()
-  | Vio2Vo ->
+  | Flags.Vio2Vo ->
       let open Filename in
       let open Library in
       Dumpglob.noglob ();
diff --git a/vernac/command.ml b/vernac/command.ml
index 32ab5401a..b611edc41 100644
--- a/vernac/command.ml
+++ b/vernac/command.ml
@@ -9,7 +9,6 @@
 open Pp
 open CErrors
 open Util
-open Flags
 open Term
 open Vars
 open Termops
@@ -692,7 +691,7 @@ let declare_mutual_inductive_with_eliminations mie pl impls =
 		constrimpls)
       impls;
   let warn_prim = match mie.mind_entry_record with Some (Some _) -> not prim | _ -> false in
-  if_verbose Feedback.msg_info (minductive_message warn_prim names);
+  Flags.if_verbose Feedback.msg_info (minductive_message warn_prim names);
   if mie.mind_entry_private == None
   then declare_default_schemes mind;
   mind
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index 645320c60..590fa6213 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -11,7 +11,6 @@
 
 open CErrors
 open Util
-open Flags
 open Pp
 open Names
 open Term
@@ -137,7 +136,7 @@ let find_mutually_recursive_statements thms =
 	  assert (List.is_empty rest);
           (* One occ. of common coind ccls and no common inductive hyps *)
 	  if not (List.is_empty common_same_indhyp) then
-	    if_verbose Feedback.msg_info (str "Assuming mutual coinductive statements.");
+	    Flags.if_verbose Feedback.msg_info (str "Assuming mutual coinductive statements.");
 	  flush_all ();
           indccl, true, []
       | [], _::_ ->
@@ -145,7 +144,7 @@ let find_mutually_recursive_statements thms =
           | ind :: _ ->
             if List.distinct_f ind_ord (List.map pi1 ind)
             then
-              if_verbose Feedback.msg_info
+              Flags.if_verbose Feedback.msg_info
                 (strbrk
                    ("Coinductive statements do not follow the order of "^
                     "definition, assuming the proof to be by induction."));
diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml
index c424b1d50..7b0d59812 100644
--- a/vernac/metasyntax.ml
+++ b/vernac/metasyntax.ml
@@ -7,7 +7,6 @@
 (************************************************************************)
 
 open Pp
-open Flags
 open CErrors
 open Util
 open Names
@@ -794,7 +793,7 @@ type notation_modifier = {
   (* common to syn_data below *)
   only_parsing  : bool;
   only_printing : bool;
-  compat        : compat_version option;
+  compat        : Flags.compat_version option;
   format        : string Loc.located option;
   extra         : (string * string) list;
 }
@@ -1073,7 +1072,7 @@ module SynData = struct
     (* Fields coming from the vernac-level modifiers *)
     only_parsing  : bool;
     only_printing : bool;
-    compat        : compat_version option;
+    compat        : Flags.compat_version option;
     format        : string Loc.located option;
     extra         : (string * string) list;
 
@@ -1389,7 +1388,7 @@ let add_notation_interpretation ((loc,df),c,sc) =
 
 let set_notation_for_interpretation impls ((_,df),c,sc) =
   (try ignore
-    (silently (fun () -> add_notation_interpretation_core false df ~impls c sc false false None) ());
+    (Flags.silently (fun () -> add_notation_interpretation_core false df ~impls c sc false false None) ());
   with NoSyntaxRule ->
     user_err Pp.(str "Parsing rule for this notation has to be previously declared."));
   Option.iter (fun sc -> Notation.open_close_scope (false,true,sc)) sc
diff --git a/vernac/mltop.ml b/vernac/mltop.ml
index e8a0ba3dd..1edbd1a85 100644
--- a/vernac/mltop.ml
+++ b/vernac/mltop.ml
@@ -9,7 +9,6 @@
 open CErrors
 open Util
 open Pp
-open Flags
 open Libobject
 open System
 
@@ -365,7 +364,7 @@ let trigger_ml_object verb cache reinit ?path name =
   else begin
     let file = file_of_name (Option.default name path) in
     let path =
-      if_verbose_load (verb && not !quiet) load_ml_object name ?path file in
+      if_verbose_load (verb && not !Flags.quiet) load_ml_object name ?path file in
     add_loaded_module name (Some path);
     if cache then perform_cache_obj name
   end
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 4fd08b42d..b0e438a8e 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -11,7 +11,6 @@
 open Pp
 open CErrors
 open Util
-open Flags
 open Names
 open Nameops
 open Term
@@ -657,7 +656,7 @@ let vernac_declare_module export (loc, id) binders_ast mty_ast =
       id binders_ast (Enforce mty_ast) []
   in
   Dumpglob.dump_moddef ?loc mp "mod";
-  if_verbose Feedback.msg_info (str "Module " ++ pr_id id ++ str " is declared");
+  Flags.if_verbose Feedback.msg_info (str "Module " ++ pr_id id ++ str " is declared");
   Option.iter (fun export -> vernac_import export [Ident (Loc.tag id)]) export
 
 let vernac_define_module export (loc, id) binders_ast mty_ast_o mexpr_ast_l =
@@ -678,7 +677,7 @@ let vernac_define_module export (loc, id) binders_ast mty_ast_o mexpr_ast_l =
            export id binders_ast mty_ast_o
        in
        Dumpglob.dump_moddef ?loc mp "mod";
-       if_verbose Feedback.msg_info
+       Flags.if_verbose Feedback.msg_info
          (str "Interactive Module " ++ pr_id id ++ str " started");
        List.iter
          (fun (export,id) ->
@@ -696,7 +695,7 @@ let vernac_define_module export (loc, id) binders_ast mty_ast_o mexpr_ast_l =
 	   id binders_ast mty_ast_o mexpr_ast_l
        in
        Dumpglob.dump_moddef ?loc mp "mod";
-       if_verbose Feedback.msg_info
+       Flags.if_verbose Feedback.msg_info
 	 (str "Module " ++ pr_id id ++ str " is defined");
        Option.iter (fun export -> vernac_import export [Ident (Loc.tag id)])
          export
@@ -704,7 +703,7 @@ let vernac_define_module export (loc, id) binders_ast mty_ast_o mexpr_ast_l =
 let vernac_end_module export (loc,id as lid) =
   let mp = Declaremods.end_module () in
   Dumpglob.dump_modref ?loc mp "mod";
-  if_verbose Feedback.msg_info (str "Module " ++ pr_id id ++ str " is defined");
+  Flags.if_verbose Feedback.msg_info (str "Module " ++ pr_id id ++ str " is defined");
   Option.iter (fun export -> vernac_import export [Ident lid]) export
 
 let vernac_declare_module_type (loc,id) binders_ast mty_sign mty_ast_l =
@@ -725,7 +724,7 @@ let vernac_declare_module_type (loc,id) binders_ast mty_sign mty_ast_l =
            id binders_ast mty_sign
        in
        Dumpglob.dump_moddef ?loc mp "modtype";
-       if_verbose Feedback.msg_info
+       Flags.if_verbose Feedback.msg_info
 	 (str "Interactive Module Type " ++ pr_id id ++ str " started");
        List.iter
          (fun (export,id) ->
@@ -744,13 +743,13 @@ let vernac_declare_module_type (loc,id) binders_ast mty_sign mty_ast_l =
 	    id binders_ast mty_sign mty_ast_l
         in
         Dumpglob.dump_moddef ?loc mp "modtype";
-	if_verbose Feedback.msg_info
+	Flags.if_verbose Feedback.msg_info
 	  (str "Module Type " ++ pr_id id ++ str " is defined")
 
 let vernac_end_modtype (loc,id) =
   let mp = Declaremods.end_modtype () in
   Dumpglob.dump_modref ?loc mp "modtype";
-  if_verbose Feedback.msg_info (str "Module Type " ++ pr_id id ++ str " is defined")
+  Flags.if_verbose Feedback.msg_info (str "Module Type " ++ pr_id id ++ str " is defined")
 
 let vernac_include l =
   Declaremods.declare_include Modintern.interp_module_ast l
@@ -818,7 +817,7 @@ let vernac_coercion locality poly local ref qids qidt =
   let source = cl_of_qualid qids in
   let ref' = smart_global ref in
   Class.try_add_new_coercion_with_target ref' ~local poly ~source ~target;
-  if_verbose Feedback.msg_info (pr_global ref' ++ str " is now a coercion")
+  Flags.if_verbose Feedback.msg_info (pr_global ref' ++ str " is now a coercion")
 
 let vernac_identity_coercion locality poly local id qids qidt =
   let local = enforce_locality locality local in
@@ -920,7 +919,7 @@ let vernac_chdir = function
 	  so we make it an error. *)
 	  user_err Pp.(str ("Cd failed: " ^ err))
       end;
-      if_verbose Feedback.msg_info (str (Sys.getcwd()))
+      Flags.if_verbose Feedback.msg_info (str (Sys.getcwd()))
 
 
 (********************)
@@ -1302,7 +1301,7 @@ let _ =
       optname  = "automatic introduction of variables";
       optkey   = ["Automatic";"Introduction"];
       optread  = Flags.is_auto_intros;
-      optwrite = make_auto_intros }
+      optwrite = Flags.make_auto_intros }
 
 let _ =
   declare_bool_option
@@ -2050,7 +2049,7 @@ let interp ?proof ?loc locality poly c =
   | VernacSearch (s,g,r) -> vernac_search ?loc s g r
   | VernacLocate l -> vernac_locate l
   | VernacRegister (id, r) -> vernac_register id r
-  | VernacComments l -> if_verbose Feedback.msg_info (str "Comments ok\n")
+  | VernacComments l -> Flags.if_verbose Feedback.msg_info (str "Comments ok\n")
 
   (* Proof management *)
   | VernacGoal t -> vernac_start_proof locality poly Theorem [None,([],t)]
@@ -2176,7 +2175,7 @@ let with_fail b f =
       | HasNotFailed ->
           user_err ~hdr:"Fail" (str "The command has not failed!")
       | HasFailed msg ->
-          if not !Flags.quiet || !test_mode || !ide_slave then Feedback.msg_info
+          if not !Flags.quiet || !Flags.test_mode || !Flags.ide_slave then Feedback.msg_info
             (str "The command has indeed failed with message:" ++ fnl () ++ msg)
       | _ -> assert false
   end