diff options
Diffstat (limited to 'dev/doc/changes.md')
-rw-r--r-- | dev/doc/changes.md | 60 |
1 files changed, 60 insertions, 0 deletions
diff --git a/dev/doc/changes.md b/dev/doc/changes.md index f3fc126f9..4177513a1 100644 --- a/dev/doc/changes.md +++ b/dev/doc/changes.md @@ -53,6 +53,16 @@ Printer.ml API pr_subgoal and pr_goal was removed to simplify the code. It was earlierly used by PCoq. +Kernel + + The following renamings happened: + - `Context.Rel.t` into `Constr.rel_context` + - `Context.Named.t` into `Constr.named_context` + - `Context.Compacted.t` into `Constr.compacted_context` + - `Context.Rel.Declaration.t` into `Constr.rel_declaration` + - `Context.Named.Declaration.t` into `Constr.named_declaration` + - `Context.Compacted.Declaration.t` into `Constr.compacted_declaration` + Source code organization - We have eliminated / fused some redundant modules and relocated a @@ -72,11 +82,61 @@ Vernacular commands `tactics/`. In all cases adapting is a matter of changing the module name. +Primitive number parsers + +- For better modularity, the primitive parsers for positive, N and Z + have been split over three files (plugins/syntax/positive_syntax.ml, + plugins/syntax/n_syntax.ml, plugins/syntax/z_syntax.ml). + ### Unit testing The test suite now allows writing unit tests against OCaml code in the Coq code base. Those unit tests create a dependency on the OUnit test framework. +### Transitioning away from Camlp5 + +In an effort to reduce dependency on Camlp5, the use of Camlp5 GEXTEND macro +is discouraged. Most plugin writers do not need this low-level interface, but +for those who do, the transition path is somewhat straightforward. To convert +a ml4 file containing only standard OCaml with GEXTEND statements, the following +should be enough: +- replace its "ml4" extension with "mlg" +- replace GEXTEND with GRAMMAR EXTEND +- wrap every occurrence of OCaml code into braces { } + +For instance, code of the form +``` +let myval = 0 + +GEXTEND Gram + GLOBAL: my_entry; + +my_entry: +[ [ x = bar; y = qux -> do_something x y + | "("; z = LIST0 my_entry; ")" -> do_other_thing z +] ]; +END +``` +should be turned into +``` +{ +let myval = 0 +} + +GRAMMAR EXTEND Gram + GLOBAL: my_entry; + +my_entry: +[ [ x = bar; y = qux -> { do_something x y } + | "("; z = LIST0 my_entry; ")" -> { do_other_thing z } +] ]; +END +``` + +Currently mlg files can only contain GRAMMAR EXTEND statements. They do not +support TACTIC, VERNAC nor ARGUMENT EXTEND. In case you have a file containing +both kinds at the same time, it is recommended splitting it in two. + ## Changes between Coq 8.7 and Coq 8.8 ### Bug tracker |