From fb482f6b02156c1fcf029263083b0371e030a2cd Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Wed, 20 Sep 2017 08:30:24 +0200
Subject: [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`
---
 vernac/command.ml | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

(limited to 'vernac/command.ml')

diff --git a/vernac/command.ml b/vernac/command.ml
index 32ab5401a0..b611edc41d 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
-- 
cgit v1.2.3