diff options
| author | Pierre-Marie Pédrot | 2015-10-25 16:27:44 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2015-10-25 16:45:14 +0100 |
| commit | af89d24f9d54b18068046545af1268dffbeb3e07 (patch) | |
| tree | b3c4a9fb2472c6428e8f63dad0b18225c4fd5902 /grammar | |
| parent | 06e10609b3bb04c3f42a2211c9f782f130ffd7dd (diff) | |
Getting rid of the Atactic entry.
Diffstat (limited to 'grammar')
| -rw-r--r-- | grammar/q_util.ml4 | 4 |
1 files changed, 2 insertions, 2 deletions
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$ >> |