3 files changed, 9 insertions, 26 deletions
diff --git a/dev/doc/changes.md b/dev/doc/changes.md
index 7d2100515d..59c1623a2d 100644
--- a/dev/doc/changes.md
+++ b/dev/doc/changes.md
@@ -4,6 +4,12 @@
   comes from a notation. Use `None` if not and `Some foo` to tell to
   print such TacGeneric surrounded with `foo:( )`.
 
+### Code formatting
+
+- The automatic code formatting tool `ocamlformat` has been disabled and its
+  git hook removed. If desired, automatic formatting can be achieved by calling
+  the `fmt` target of the dune build system.
+
 ## Changes between Coq 8.11 and Coq 8.12
 
 ### Code formatting
diff --git a/dev/lint-repository.sh b/dev/lint-repository.sh
index 553696410c..2e8a7455de 100755
--- a/dev/lint-repository.sh
+++ b/dev/lint-repository.sh
@@ -32,7 +32,4 @@ find . "(" -path ./.git -prune ")" -o -type f -print0 |
 echo Checking overlays
 dev/tools/check-overlays.sh || CODE=1
 
-echo Checking ocamlformat
-make -f Makefile.dune fmt || CODE=1
-
 exit $CODE
diff --git a/dev/tools/pre-commit b/dev/tools/pre-commit
index 448e224f2e..74fcceb038 100755
--- a/dev/tools/pre-commit
+++ b/dev/tools/pre-commit
@@ -7,25 +7,7 @@ set -e
 
 dev/tools/check-overlays.sh
 
-# Can we check and fix formatting?
-# NB: we will ignore errors from ocamlformat as it fails when
-# encountering OCaml syntax errors
-ocamlformat=$(command -v ocamlformat || echo true)
-if [ "$ocamlformat" = true ]
-then
-    1>&2 echo "Warning: ocamlformat is not in path. Cannot check formatting."
-fi
-
-# Verify that the version of ocamlformat matches the one in .ocamlformat
-# The following command will print an error message if that's not the case
-# (and will print nothing if the versions match)
-if ! echo "let () = ()" | "$ocamlformat" --impl - > /dev/null
-then
-    1>&2 echo "Warning: Cannot check formatting."
-    ocamlformat=true
-fi
-
-1>&2 echo "Auto fixing whitespace and formatting issues..."
+1>&2 echo "Auto fixing whitespace issues..."
 
 # We fix whitespace in the index and in the working tree
 # separately to preserve non-added changes.
@@ -52,7 +34,6 @@ if [ -s "$index" ]; then
     git apply --cached --whitespace=fix "$index"
     git apply --whitespace=fix "$index" 2>/dev/null # no need to repeat yourself
     git diff --cached --name-only -z | xargs -0 dev/tools/check-eof-newline.sh --fix
-    { git diff --cached --name-only -z | grep -E '.*\.mli?$' -z | xargs -0 "$ocamlformat" -i || true; } 2> /dev/null
     git add -u
     1>&2 echo #newline
 fi
@@ -68,12 +49,11 @@ if [ -s "$tree" ]; then
     1>&2 echo "Fixing unstaged changes..."
     git apply --whitespace=fix "$tree"
     git diff --name-only -z | xargs -0 dev/tools/check-eof-newline.sh --fix
-    { git diff --name-only -z | grep -E '.*\.mli?$' -z | xargs -0 "$ocamlformat" -i || true; } 2> /dev/null
     1>&2 echo #newline
 fi
 
 if [ -s "$index" ] && ! [ -s "$fixed_index" ]; then
-    1>&2 echo "Fixing whitespace and formatting issues cancelled all changes."
+    1>&2 echo "Fixing whitespace issues cancelled all changes."
     exit 1
 fi
 
@@ -84,7 +64,7 @@ if ! git diff-index --check --cached HEAD; then
     1>&2 echo "(Consider whether the number of errors decreases after each run.)"
     exit 1
 fi
-1>&2 echo "Whitespace and formatting pass complete."
+1>&2 echo "Whitespace pass complete."
 
 # clean up temporary files
 rm "$index" "$tree" "$fixed_index"