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/metasyntax.ml | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) (limited to 'vernac/metasyntax.ml') 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 -- cgit v1.2.3