aboutsummaryrefslogtreecommitdiffhomepage
path: root/grammar/q_util.ml4
diff options
context:
space:
mode:
Diffstat (limited to 'grammar/q_util.ml4')
-rw-r--r--grammar/q_util.ml42
1 files changed, 1 insertions, 1 deletions
diff --git a/grammar/q_util.ml4 b/grammar/q_util.ml4
index eee84c38d..34f1cf6cb 100644
--- a/grammar/q_util.ml4
+++ b/grammar/q_util.ml4
@@ -59,6 +59,6 @@ let rec mlexpr_of_prod_entry_key = function
| 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 "Agram not supported"
+ | Pcoq.Agram s -> Errors.anomaly (Pp.str "Agram not supported")
| Pcoq.Aentry ("",s) -> <:expr< Pcoq.Agram (Pcoq.Gram.Entry.obj $lid:s$) >>
| Pcoq.Aentry (u,s) -> <:expr< Pcoq.Aentry $str:u$ $str:s$ >>