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`.
---
 parsing/g_vernac.ml4 | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

(limited to 'parsing')

diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index b9a162bec5..7a7746cc9c 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -1134,14 +1134,13 @@ GEXTEND Gram
 
      | IDENT "Reserved"; IDENT "Infix"; s = ne_lstring;
 	 l = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> [] ] ->
-	   Metasyntax.check_infix_modifiers l;
 	   let (loc,s) = s in
-	   VernacSyntaxExtension (false,((loc,"x '"^s^"' y"),l))
+	   VernacSyntaxExtension (true, false,((loc,"x '"^s^"' y"),l))
 
      | IDENT "Reserved"; IDENT "Notation"; local = obsolete_locality;
 	 s = ne_lstring;
 	 l = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> [] ]
-	 -> VernacSyntaxExtension (local,(s,l))
+	 -> VernacSyntaxExtension (false, local,(s,l))
 
      (* "Print" "Grammar" should be here but is in "command" entry in order
         to factorize with other "Print"-based vernac entries *)
-- 
cgit v1.2.3


From 028de158153de94adfcb9d1e995259d833968951 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Mon, 31 Jul 2017 14:24:11 +0200
Subject: [general] Merge parsing with highparsing, put toplevel at the top of
 the linking chain.

---
 parsing/highparsing.mllib | 4 ----
 parsing/parsing.mllib     | 4 ++++
 2 files changed, 4 insertions(+), 4 deletions(-)
 delete mode 100644 parsing/highparsing.mllib

(limited to 'parsing')

diff --git a/parsing/highparsing.mllib b/parsing/highparsing.mllib
deleted file mode 100644
index 05e2911c2f..0000000000
--- a/parsing/highparsing.mllib
+++ /dev/null
@@ -1,4 +0,0 @@
-G_constr
-G_vernac
-G_prim
-G_proofs
diff --git a/parsing/parsing.mllib b/parsing/parsing.mllib
index 2a73d7bc69..1f29636b2e 100644
--- a/parsing/parsing.mllib
+++ b/parsing/parsing.mllib
@@ -3,3 +3,7 @@ CLexer
 Pcoq
 Egramml
 Egramcoq
+G_constr
+G_vernac
+G_prim
+G_proofs
-- 
cgit v1.2.3