diff options
Diffstat (limited to 'dev/top_printers.ml')
| -rw-r--r-- | dev/top_printers.ml | 20 |
1 files changed, 8 insertions, 12 deletions
diff --git a/dev/top_printers.ml b/dev/top_printers.ml index 5e3fbb6167..4881c3eefa 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -400,12 +400,10 @@ let _ = e -> Pp.pp (Cerrors.explain_exn e) let _ = extend_vernac_command_grammar "PrintConstr" - [[TacTerm "PrintConstr"; - TacNonTerm - (dummy_loc, - (Gramext.Snterm (Pcoq.Gram.Entry.obj Constr.constr), - ConstrArgType), - Some "c")]] + [[GramTerminal "PrintConstr"; + GramNonTerminal + (dummy_loc,ConstrArgType,Extend.Aentry ("constr","constr"), + Some (Names.id_of_string "c"))]] let _ = try @@ -419,12 +417,10 @@ let _ = e -> Pp.pp (Cerrors.explain_exn e) let _ = extend_vernac_command_grammar "PrintPureConstr" - [[TacTerm "PrintPureConstr"; - TacNonTerm - (dummy_loc, - (Gramext.Snterm (Pcoq.Gram.Entry.obj Constr.constr), - ConstrArgType), - Some "c")]] + [[GramTerminal "PrintPureConstr"; + GramNonTerminal + (dummy_loc,ConstrArgType,Extend.Aentry ("constr","constr"), + Some (Names.id_of_string "c"))]] (* Setting printer of unbound global reference *) open Names |