diff options
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 3b5490e31..5298ef2e4 100644 --- a/vernac/metasyntax.ml +++ b/vernac/metasyntax.ml @@ -7,7 +7,6 @@ (************************************************************************) open Pp -open Flags open CErrors open Util open Names @@ -802,7 +801,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; } @@ -1081,7 +1080,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; @@ -1397,7 +1396,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 |