From 6150d15647afc739329019f7e9de595187ecc282 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 9 May 2016 16:08:50 +0200
Subject: Removing the Entry module now that rules need not be marshalled.

---
 grammar/q_util.ml4 | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'grammar/q_util.ml4')

diff --git a/grammar/q_util.ml4 b/grammar/q_util.ml4
index c529260e9d..05c94394d3 100644
--- a/grammar/q_util.ml4
+++ b/grammar/q_util.ml4
@@ -71,8 +71,8 @@ let rec mlexpr_of_prod_entry_key f = function
   | Uentryl (e, l) ->
     (** Keep in sync with Pcoq! *)
     assert (e = "tactic");
-    if l = 5 then <:expr< Extend.Aentry (Pcoq.name_of_entry Pcoq.Tactic.binder_tactic) >>
-    else <:expr< Extend.Aentryl (Pcoq.name_of_entry Pcoq.Tactic.tactic_expr) $mlexpr_of_int l$ >>
+    if l = 5 then <:expr< Extend.Aentry (Pcoq.Tactic.binder_tactic) >>
+    else <:expr< Extend.Aentryl (Pcoq.Tactic.tactic_expr) $mlexpr_of_int l$ >>
 
 let rec type_of_user_symbol = function
 | Ulist1 s | Ulist1sep (s, _) | Ulist0 s | Ulist0sep (s, _) ->
-- 
cgit v1.2.3


From 61f79019be6082c3ebabd503c322fb2edb05a99a Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 10 May 2016 11:11:39 +0200
Subject: AlistNsep token now accepts an arbitrary separator.

---
 grammar/q_util.ml4 | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

(limited to 'grammar/q_util.ml4')

diff --git a/grammar/q_util.ml4 b/grammar/q_util.ml4
index 05c94394d3..53330429d9 100644
--- a/grammar/q_util.ml4
+++ b/grammar/q_util.ml4
@@ -61,11 +61,13 @@ let mlexpr_of_option f = function
 let mlexpr_of_ident id =
   <:expr< Names.Id.of_string $str:id$ >>
 
+let symbol_of_string s = <:expr< Extend.Atoken (CLexer.terminal $str:s$) >>
+
 let rec mlexpr_of_prod_entry_key f = function
   | Ulist1 s -> <:expr< Extend.Alist1 $mlexpr_of_prod_entry_key f s$ >>
-  | Ulist1sep (s,sep) -> <:expr< Extend.Alist1sep $mlexpr_of_prod_entry_key f s$ $str:sep$ >>
+  | Ulist1sep (s,sep) -> <:expr< Extend.Alist1sep $mlexpr_of_prod_entry_key f s$ $symbol_of_string sep$ >>
   | Ulist0 s -> <:expr< Extend.Alist0 $mlexpr_of_prod_entry_key f s$ >>
-  | Ulist0sep (s,sep) -> <:expr< Extend.Alist0sep $mlexpr_of_prod_entry_key f s$ $str:sep$ >>
+  | Ulist0sep (s,sep) -> <:expr< Extend.Alist0sep $mlexpr_of_prod_entry_key f s$ $symbol_of_string sep$ >>
   | Uopt s -> <:expr< Extend.Aopt $mlexpr_of_prod_entry_key f s$ >>
   | Uentry e -> <:expr< Extend.Aentry $f e$ >>
   | Uentryl (e, l) ->
-- 
cgit v1.2.3