diff options
| author | Pierre-Marie Pédrot | 2014-09-09 22:13:08 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2014-09-10 00:16:20 +0200 |
| commit | edfa5e986a25eb7a0719d20b43a618cb5bd4cd95 (patch) | |
| tree | e7af11e344a99b2496d22d2bc100f493bd701b96 /dev | |
| parent | 0dd3f0d34873dcd126be8ec48724a310214f38ac (diff) | |
VernacExtend does not dispatch on type anymore.
Diffstat (limited to 'dev')
| -rw-r--r-- | dev/top_printers.ml | 16 |
1 files changed, 8 insertions, 8 deletions
diff --git a/dev/top_printers.ml b/dev/top_printers.ml index 15f35b775f..56c71d88f5 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -476,7 +476,7 @@ open Egramml let _ = try - Vernacinterp.vinterp_add "PrintConstr" + Vernacinterp.vinterp_add ("PrintConstr", 0) (function [c] when genarg_tag c = ConstrArgType && true -> let c = out_gen (rawwit wit_constr) c in @@ -485,15 +485,15 @@ let _ = with e -> Pp.pp (Errors.print e) let _ = - extend_vernac_command_grammar "PrintConstr" None - [[GramTerminal "PrintConstr"; + extend_vernac_command_grammar ("PrintConstr", 0) None + [GramTerminal "PrintConstr"; GramNonTerminal (Loc.ghost,ConstrArgType,Aentry ("constr","constr"), - Some (Names.Id.of_string "c"))]] + Some (Names.Id.of_string "c"))] let _ = try - Vernacinterp.vinterp_add "PrintPureConstr" + Vernacinterp.vinterp_add ("PrintPureConstr", 0) (function [c] when genarg_tag c = ConstrArgType && true -> let c = out_gen (rawwit wit_constr) c in @@ -502,11 +502,11 @@ let _ = with e -> Pp.pp (Errors.print e) let _ = - extend_vernac_command_grammar "PrintPureConstr" None - [[GramTerminal "PrintPureConstr"; + extend_vernac_command_grammar ("PrintPureConstr", 0) None + [GramTerminal "PrintPureConstr"; GramNonTerminal (Loc.ghost,ConstrArgType,Aentry ("constr","constr"), - Some (Names.Id.of_string "c"))]] + Some (Names.Id.of_string "c"))] (* Setting printer of unbound global reference *) open Names |