diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-10-24 23:58:28 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-10-25 00:11:48 +0200 |
| commit | 06e10609b3bb04c3f42a2211c9f782f130ffd7dd (patch) | |
| tree | 35c4084502188939cb7af36d1197d4d1a6b30146 /grammar/q_util.ml4 | |
| parent | d0530179206ff98a327bc189139f75b83ece35ed (diff) | |
Getting rid of the Agram entry.
Diffstat (limited to 'grammar/q_util.ml4')
| -rw-r--r-- | grammar/q_util.ml4 | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/grammar/q_util.ml4 b/grammar/q_util.ml4 index b1eabdd98..5b005186b 100644 --- a/grammar/q_util.ml4 +++ b/grammar/q_util.ml4 @@ -59,6 +59,5 @@ let rec mlexpr_of_prod_entry_key : type s a. (s, a) Pcoq.entry_key -> _ = functi | Pcoq.Aself -> <:expr< Pcoq.Aself >> | Pcoq.Anext -> <:expr< Pcoq.Anext >> | Pcoq.Atactic n -> <:expr< Pcoq.Atactic $mlexpr_of_int n$ >> - | Pcoq.Agram s -> Errors.anomaly (Pp.str "Agram not supported") - | Pcoq.Aentry ("",s) -> <:expr< Pcoq.Agram (Pcoq.Gram.Entry.name $lid:s$) >> + | Pcoq.Aentry ("",s) -> <:expr< Pcoq.Aentry (Pcoq.name_of_entry $lid:s$) >> | Pcoq.Aentry (u,s) -> <:expr< Pcoq.Aentry $str:u$ $str:s$ >> |