diff options
Diffstat (limited to 'dev')
| -rw-r--r-- | dev/doc/changes.txt | 4 | ||||
| -rw-r--r-- | dev/printers.mllib | 1 | ||||
| -rw-r--r-- | dev/top_printers.ml | 20 |
3 files changed, 13 insertions, 12 deletions
diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt index a9673664a..c82e1e652 100644 --- a/dev/doc/changes.txt +++ b/dev/doc/changes.txt @@ -2,6 +2,10 @@ = CHANGES BETWEEN COQ V8.2 AND COQ V8.3 = ========================================= +** Cleaning in parsing extensions (commit ) + +Many moves and renamings, one new file (Extrawit, that contains wit_tactic). + ** Cleaning in tactical.mli tclLAST_HYP -> onLastHyp diff --git a/dev/printers.mllib b/dev/printers.mllib index 25ec05fba..f4b3d7f6c 100644 --- a/dev/printers.mllib +++ b/dev/printers.mllib @@ -112,6 +112,7 @@ Tactic_debug Decl_mode Ppconstr Extend +Extrawit Pcoq Printer Pptactic diff --git a/dev/top_printers.ml b/dev/top_printers.ml index 5e3fbb616..4881c3eef 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 |