diff options
Diffstat (limited to 'grammar')
| -rw-r--r-- | grammar/argextend.ml4 | 4 | ||||
| -rw-r--r-- | grammar/q_util.ml4 | 2 |
2 files changed, 3 insertions, 3 deletions
diff --git a/grammar/argextend.ml4 b/grammar/argextend.ml4 index c11ffddbf..4d9904694 100644 --- a/grammar/argextend.ml4 +++ b/grammar/argextend.ml4 @@ -261,8 +261,8 @@ let declare_vernac_argument loc s pr cl = (None, [(None, None, $rules$)]); Pptactic.declare_extra_genarg_pprule ($rawwit$, $pr_rules$) - ($globwit$, fun _ _ _ _ -> Errors.anomaly "vernac argument needs not globwit printer") - ($wit$, fun _ _ _ _ -> Errors.anomaly "vernac argument needs not wit printer") } + ($globwit$, fun _ _ _ _ -> Errors.anomaly (Pp.str "vernac argument needs not globwit printer")) + ($wit$, fun _ _ _ _ -> Errors.anomaly (Pp.str "vernac argument needs not wit printer")) } >> ] open Pcoq 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$ >> |