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`.
---
 intf/vernacexpr.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'intf')

diff --git a/intf/vernacexpr.ml b/intf/vernacexpr.ml
index 2adf522b74..8b6abb6e82 100644
--- a/intf/vernacexpr.ml
+++ b/intf/vernacexpr.ml
@@ -325,7 +325,7 @@ type vernac_expr =
 
   (* Syntax *)
   | VernacSyntaxExtension of
-      obsolete_locality * (lstring * syntax_modifier list)
+      bool * obsolete_locality * (lstring * syntax_modifier list)
   | VernacOpenCloseScope of obsolete_locality * (bool * scope_name)
   | VernacDelimiters of scope_name * string option
   | VernacBindScope of scope_name * class_rawexpr list
-- 
cgit v1.2.3