diff options
| author | Pierre-Marie Pédrot | 2017-07-31 14:22:48 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2017-08-29 17:39:40 +0200 |
| commit | cc58638a8d33084c5c9f85ab4d536307da2d7929 (patch) | |
| tree | 5b12f123aea95ae02d1f18d8c3226ec2892d001f /vernac | |
| parent | 73d577c2d959de975415f2807df6a22fa392d335 (diff) | |
[vernac] Store Infix Modifier in Vernac Notation.
This removes a dependency from `G_vernac` to `Metasyntax`.
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/vernacentries.ml | 9 |
1 files changed, 5 insertions, 4 deletions
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 8738e58e82..8322958f72 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -409,9 +409,10 @@ let dump_global r = (**********) (* Syntax *) -let vernac_syntax_extension locality local = +let vernac_syntax_extension locality local infix l = let local = enforce_module_locality locality local in - Metasyntax.add_syntax_extension local + if infix then Metasyntax.check_infix_modifiers (snd l); + Metasyntax.add_syntax_extension local l let vernac_delimiters sc = function | Some lr -> Metasyntax.add_delimiters sc lr @@ -1950,8 +1951,8 @@ let interp ?proof ?loc locality poly c = | VernacLocal _ -> assert false (* Syntax *) - | VernacSyntaxExtension (local,sl) -> - vernac_syntax_extension locality local sl + | VernacSyntaxExtension (infix, local,sl) -> + vernac_syntax_extension locality local infix sl | VernacDelimiters (sc,lr) -> vernac_delimiters sc lr | VernacBindScope (sc,rl) -> vernac_bind_scope sc rl | VernacOpenCloseScope (local, s) -> vernac_open_close_scope locality local s |