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/argextend.ml4    | 2 +-
 grammar/q_util.ml4       | 4 ++--
 grammar/vernacextend.ml4 | 2 +-
 3 files changed, 4 insertions(+), 4 deletions(-)

(limited to 'grammar')

diff --git a/grammar/argextend.ml4 b/grammar/argextend.ml4
index 0e52dc948a..9be6c6bc4a 100644
--- a/grammar/argextend.ml4
+++ b/grammar/argextend.ml4
@@ -42,7 +42,7 @@ let make_act loc act pil =
 let make_prod_item = function
   | ExtTerminal s -> <:expr< Extend.Atoken (CLexer.terminal $mlexpr_of_string s$) >>
   | ExtNonTerminal (g, _) ->
-    let base s = <:expr< Pcoq.name_of_entry $lid:s$ >> in
+    let base s = <:expr< $lid:s$ >> in
     mlexpr_of_prod_entry_key base g
 
 let rec make_prod = function
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, _) ->
diff --git a/grammar/vernacextend.ml4 b/grammar/vernacextend.ml4
index 0d4bec69d5..904662ea1c 100644
--- a/grammar/vernacextend.ml4
+++ b/grammar/vernacextend.ml4
@@ -106,7 +106,7 @@ let make_prod_item = function
   | ExtTerminal s -> <:expr< Egramml.GramTerminal $str:s$ >>
   | ExtNonTerminal (g, id) ->
     let nt = type_of_user_symbol g in
-    let base s = <:expr< Pcoq.name_of_entry (Pcoq.genarg_grammar $mk_extraarg loc s$) >> in
+    let base s = <:expr< Pcoq.genarg_grammar ($mk_extraarg loc s$) >> in
       <:expr< Egramml.GramNonTerminal $default_loc$ $make_rawwit loc nt$
       $mlexpr_of_prod_entry_key base g$ >>
 
-- 
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')

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