diff options
Diffstat (limited to 'dev/doc')
| -rw-r--r-- | dev/doc/build-system.dune.md | 7 | ||||
| -rw-r--r-- | dev/doc/changes.md | 22 |
2 files changed, 21 insertions, 8 deletions
diff --git a/dev/doc/build-system.dune.md b/dev/doc/build-system.dune.md index 777eec97c6..0506216541 100644 --- a/dev/doc/build-system.dune.md +++ b/dev/doc/build-system.dune.md @@ -125,10 +125,9 @@ dune exec -- dev/dune-dbg checker foo.vo (ocd) source dune_db ``` -Unfortunately, dependency handling here is not fully refined, so you -need to build enough of Coq once to use this target [it will then -correctly compute the deps and rebuild if you call the script again] -This will be fixed in the future. +Unfortunately, dependency handling is not fully refined / automated, +you may find the occasional hiccup due to libraries being renamed, +etc... Please report any issue. For running in emacs, use `coqdev-ocamldebug` from `coqdev.el`. diff --git a/dev/doc/changes.md b/dev/doc/changes.md index d5938713d6..eac8d86b0a 100644 --- a/dev/doc/changes.md +++ b/dev/doc/changes.md @@ -1,13 +1,22 @@ ## Changes between Coq 8.11 and Coq 8.12 -### ML API +### Code formatting -Types `precedence`, `parenRelation`, `tolerability` in -`notgram_ops.ml` have been reworked. See `entry_level` and -`entry_relative_level` in `constrexpr.ml`. +- The automatic code formatting tool `ocamlformat` is enabled now for + the micromega codebase. Version 0.13.0 is required. See + `ocalmformat`'s documentation for more details on integration with + your editor. ### ML API +Notations: + +- Most operators on numerals have moved to file numTok.ml. + +- Types `precedence`, `parenRelation`, `tolerability` in + `notgram_ops.ml` have been reworked. See `entry_level` and + `entry_relative_level` in `constrexpr.ml`. + Exception handling: - Coq's custom `Backtrace` module has been removed in favor of OCaml's @@ -21,6 +30,11 @@ Exception handling: + printers are of type `exn -> Pp.t option` [`None` == not handled] + it is forbidden for exception printers to raise. +- Refiner.catchable_exception is deprecated, use instead + CErrors.noncritical in try-with block. Note that nothing is needed in + tclORELSE block since the exceptions there are supposed to be + non-critical by construction. + Printers: - Functions such as Printer.pr_lconstr_goal_style_env have been |