diff options
Diffstat (limited to 'dev/doc')
| -rw-r--r-- | dev/doc/build-system.dune.md | 11 | ||||
| -rw-r--r-- | dev/doc/changes.md | 31 |
2 files changed, 41 insertions, 1 deletions
diff --git a/dev/doc/build-system.dune.md b/dev/doc/build-system.dune.md index 7349360be8..91ab57f1e9 100644 --- a/dev/doc/build-system.dune.md +++ b/dev/doc/build-system.dune.md @@ -107,6 +107,17 @@ global options --- such as flags --- on all packages, or build Coq with different OPAM switches simultaneously [for example to test compatibility]; for more information, please refer to the Dune manual. +## Inlining reports + +The `ireport` profile will produce standard OCaml [inlining +reports](https://caml.inria.fr/pub/docs/manual-ocaml/flambda.html#sec488). These +are to be found under `_build/default/$lib/$lib.objs/$module.$round.inlining.org` +and are in Emacs `org-mode` format. + +Note that due to https://github.com/ocaml/dune/issues/1401 , we must +perform a full rebuild each time as otherwise Dune will remove the +files. We hope to solve this in the future. + ## Documentation and test targets The documentation and test suite targets for Coq are still not 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 |