diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-09-20 08:30:24 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-09-20 08:30:24 +0200 |
| commit | fb482f6b02156c1fcf029263083b0371e030a2cd (patch) | |
| tree | 99f3ee49f015b2859f627cf2e57db0eb5ef3cb27 /vernac/metasyntax.ml | |
| parent | 9933871efd122163f7e2dfe8377b9b2dd384b47b (diff) | |
[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`
Diffstat (limited to 'vernac/metasyntax.ml')
| -rw-r--r-- | vernac/metasyntax.ml | 7 |
1 files changed, 3 insertions, 4 deletions
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 |