From af89d24f9d54b18068046545af1268dffbeb3e07 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 25 Oct 2015 16:27:44 +0100
Subject: Getting rid of the Atactic entry.

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

(limited to 'grammar')

diff --git a/grammar/q_util.ml4 b/grammar/q_util.ml4
index 5b005186bd..20c83dfafa 100644
--- a/grammar/q_util.ml4
+++ b/grammar/q_util.ml4
@@ -58,6 +58,6 @@ let rec mlexpr_of_prod_entry_key : type s a. (s, a) Pcoq.entry_key -> _ = functi
   | Pcoq.Amodifiers s -> <:expr< Pcoq.Amodifiers $mlexpr_of_prod_entry_key s$ >>
   | Pcoq.Aself -> <:expr< Pcoq.Aself >>
   | Pcoq.Anext -> <:expr< Pcoq.Anext >>
-  | Pcoq.Atactic n -> <:expr< Pcoq.Atactic $mlexpr_of_int n$ >>
   | Pcoq.Aentry ("",s) -> <:expr< Pcoq.Aentry (Pcoq.name_of_entry $lid:s$) >>
-  | Pcoq.Aentry (u,s) -> <:expr< Pcoq.Aentry $str:u$ $str:s$ >>
+  | Pcoq.Aentry (u,s) -> <:expr< Pcoq.Aentry ($str:u$, $str:s$) >>
+  | Pcoq.Aentryl ((u,s), l) -> <:expr< Pcoq.Aentryl ($str:u$, $str:s$) $mlexpr_of_int l$ >>
-- 
cgit v1.2.3