diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-11-01 22:54:24 +0100 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-11-02 11:19:08 +0100 |
| commit | 767816eece27e6bb8cba0bbf122507bd2a3b77a1 (patch) | |
| tree | 6348c7ac8f50e4782a41072e5db26d83b3b1a3a5 /grammar | |
| parent | 0df9c751f98d2f9b4423eb1bee17730cd0bf0123 (diff) | |
Using a specific function to register vernac printers.
Diffstat (limited to 'grammar')
| -rw-r--r-- | grammar/argextend.mlp | 7 |
1 files changed, 1 insertions, 6 deletions
diff --git a/grammar/argextend.mlp b/grammar/argextend.mlp index 12b7b171b..9742a002d 100644 --- a/grammar/argextend.mlp +++ b/grammar/argextend.mlp @@ -186,12 +186,7 @@ let declare_vernac_argument loc s pr cl = value ($lid:"wit_"^s$ : Genarg.genarg_type 'a unit unit) = Genarg.create_arg $se$ >>; make_extend loc s cl wit; - <:str_item< do { - Pptactic.declare_extra_genarg_pprule $wit$ - $pr_rules$ - (fun _ _ _ _ -> CErrors.anomaly (Pp.str "vernac argument needs not globwit printer.")) - (fun _ _ _ _ -> CErrors.anomaly (Pp.str "vernac argument needs not wit printer.")) } - >> ] + <:str_item< Pptactic.declare_extra_vernac_genarg_pprule $wit$ $pr_rules$ >> ] open Pcaml |