diff options
Diffstat (limited to 'dev')
| -rw-r--r-- | dev/doc/changes.md | 31 | ||||
| -rw-r--r-- | dev/top_printers.ml | 4 |
2 files changed, 32 insertions, 3 deletions
diff --git a/dev/doc/changes.md b/dev/doc/changes.md index 7e64f80ac5..f30b4107b6 100644 --- a/dev/doc/changes.md +++ b/dev/doc/changes.md @@ -19,6 +19,14 @@ Names Constant.make3 has been removed, use Constant.make2 Constant.repr3 has been removed, use Constant.repr2 +Coqlib: + +- Most functions from the `Coqlib` module have been deprecated in favor of + `register_ref` and `lib_ref`. The first one is available through the + vernacular `Register` command; it binds a name to a constant. The second + command then enables to locate the registered constant through its name. The + name resolution is dynamic. + ## Changes between Coq 8.8 and Coq 8.9 ### ML API @@ -176,7 +184,28 @@ END #### VERNAC EXTEND -Not handled yet. +Steps to perform: +- replace the brackets enclosing OCaml code in actions and rule classifiers with + braces +- if not there yet, add a leading `|̀ to the first rule + +Handwritten classifiers declared through the `CLASSIFIED BY` statement are +considered OCaml code, so they also need to be wrapped in braces. + +For instance, code of the form: +``` +VERNAC COMMAND EXTEND my_command CLASSIFIED BY classifier + [ "foo" int(i) ] => [ classif' ] -> [ cmd1 i ] +| [ "bar" ] -> [ cmd2 ] +END +``` +should be turned into +``` +VERNAC COMMAND EXTEND my_command CLASSIFIED BY { classifier } +| [ "foo" int(i) ] => { classif' } -> { cmd1 i } +| [ "bar" ] -> { cmd2 } +END +``` #### ARGUMENT EXTEND diff --git a/dev/top_printers.ml b/dev/top_printers.ml index 8129a4a867..44d44ccc4b 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -527,7 +527,7 @@ let _ = extend_vernac_command_grammar ("PrintConstr", 0) None [GramTerminal "PrintConstr"; GramNonTerminal - (Loc.tag (Some (rawwit wit_constr),Extend.Aentry Pcoq.Constr.constr))] + (Loc.tag (rawwit wit_constr,Extend.Aentry Pcoq.Constr.constr))] let _ = try @@ -543,7 +543,7 @@ let _ = extend_vernac_command_grammar ("PrintPureConstr", 0) None [GramTerminal "PrintPureConstr"; GramNonTerminal - (Loc.tag (Some (rawwit wit_constr),Extend.Aentry Pcoq.Constr.constr))] + (Loc.tag (rawwit wit_constr,Extend.Aentry Pcoq.Constr.constr))] (* Setting printer of unbound global reference *) open Names |