aboutsummaryrefslogtreecommitdiff
path: root/dev/doc
diff options
context:
space:
mode:
authorEmilio Jesus Gallego Arias2020-03-08 03:32:25 -0400
committerEmilio Jesus Gallego Arias2020-03-19 17:22:01 -0400
commit773e0a0cb5f612d9c9dc3ab4d5e850bc8c5e5e1c (patch)
treee74b301304965fdf991c678f248d1d4cb737fa25 /dev/doc
parent9f680f776140c8b3b8f79013262d5bd73761d571 (diff)
[ocamformat] Update to 0.13.0
We include the `version=0.13.0` field that should help users not to use the wrong version. `disable=true` still seems a noop with `dune`. There are some minor changes in the way comments are formatted; I'm unsure if this is due to the `wrap-comments` option; as always; tweaks to the config are most welcome.
Diffstat (limited to 'dev/doc')
-rw-r--r--dev/doc/changes.md23
1 files changed, 14 insertions, 9 deletions
diff --git a/dev/doc/changes.md b/dev/doc/changes.md
index 9088df6856..b82388675c 100644
--- a/dev/doc/changes.md
+++ b/dev/doc/changes.md
@@ -1,19 +1,19 @@
## Changes between Coq 8.11 and Coq 8.12
-### ML API
+### Code formatting
-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.
+- 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
-Types `precedence`, `parenRelation`, `tolerability` in
-`notgram_ops.ml` have been reworked. See `entry_level` and
-`entry_relative_level` in `constrexpr.ml`.
+Notations:
-### ML API
+- Types `precedence`, `parenRelation`, `tolerability` in
+ `notgram_ops.ml` have been reworked. See `entry_level` and
+ `entry_relative_level` in `constrexpr.ml`.
Exception handling:
@@ -28,6 +28,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