From cc58638a8d33084c5c9f85ab4d536307da2d7929 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 31 Jul 2017 14:22:48 +0200
Subject: [vernac] Store Infix Modifier in Vernac Notation.

This removes a dependency from `G_vernac` to `Metasyntax`.
---
 vernac/vernacentries.ml | 9 +++++----
 1 file changed, 5 insertions(+), 4 deletions(-)

(limited to 'vernac')

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
-- 
cgit v1.2.3