diff options
Diffstat (limited to 'grammar/argextend.ml4')
| -rw-r--r-- | grammar/argextend.ml4 | 4 |
1 files changed, 2 insertions, 2 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 |