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`
---
 pretyping/classops.ml | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

(limited to 'pretyping/classops.ml')

diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index 1cc072a2a2..260cd04446 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 = {
-- 
cgit v1.2.3