From 773e0a0cb5f612d9c9dc3ab4d5e850bc8c5e5e1c Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Sun, 8 Mar 2020 03:32:25 -0400
Subject: [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.
---
 dev/ci/docker/bionic_coq/Dockerfile |  4 ++--
 dev/doc/changes.md                  | 23 ++++++++++++++---------
 2 files changed, 16 insertions(+), 11 deletions(-)

(limited to 'dev')

diff --git a/dev/ci/docker/bionic_coq/Dockerfile b/dev/ci/docker/bionic_coq/Dockerfile
index e14f634073..e56e4d38ea 100644
--- a/dev/ci/docker/bionic_coq/Dockerfile
+++ b/dev/ci/docker/bionic_coq/Dockerfile
@@ -1,4 +1,4 @@
-# CACHEKEY: "bionic_coq-V2020-03-19-V93"
+# CACHEKEY: "bionic_coq-V2020-03-19-V29"
 # ^^ Update when modifying this file.
 
 FROM ubuntu:bionic
@@ -57,7 +57,7 @@ RUN opam switch create "${COMPILER}+32bit" && eval $(opam env) && \
 
 # EDGE switch
 ENV COMPILER_EDGE="4.09.1" \
-    BASE_OPAM_EDGE="dune-release.1.3.3 ocamlformat.0.12"
+    BASE_OPAM_EDGE="dune-release.1.3.3 ocamlformat.0.13.0"
 
 # EDGE+flambda switch, we install CI_OPAM as to be able to use
 # `ci-template-flambda` with everything.
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
-- 
cgit v1.2.3