7 files changed, 75 insertions, 1 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 6f79fe0a27..935d5fda84 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -310,7 +310,8 @@ lint:
   dependencies: []
   variables:
     GIT_DEPTH: "" # we need an unknown amount of history for per-commit linting
-    OPAM_SWITCH: base
+    OPAM_SWITCH: "edge"
+    OPAM_VARIANT: "+flambda"
 
 pkg:opam:
   stage: stage-1
diff --git a/.ocamlformat b/.ocamlformat
new file mode 100644
index 0000000000..3c6f577afd
--- /dev/null
+++ b/.ocamlformat
@@ -0,0 +1,6 @@
+profile=ocamlformat
+module-item-spacing=compact
+sequence-style=terminator
+cases-exp-indent=2
+field-space=loose
+exp-grouping=preserve
diff --git a/.ocamlformat-ignore b/.ocamlformat-ignore
new file mode 100644
index 0000000000..af9d896319
--- /dev/null
+++ b/.ocamlformat-ignore
@@ -0,0 +1,52 @@
+configure.ml
+dev/*
+coqpp/*
+lib/*
+clib/*
+config/*
+checker/*
+kernel/*
+library/*
+engine/*
+gramlib/*
+parsing/*
+interp/*
+pretyping/*
+printing/*
+proofs/*
+stm/*
+tactics/*
+theories/*
+user-contrib/*/*
+vernac/*
+toplevel/*
+topbin/*
+ide/*
+ide/*/*
+doc/plugin_tutorial/*/*/*
+doc/tools/docgram/*
+test-suite/*
+test-suite/*/*/*
+test-suite/*/*/*/*
+test-suite/*/*/*/*/*
+tools/*
+tools/*/*
+plugins/btauto/*
+plugins/cc/*
+plugins/derive/*
+plugins/extraction/*
+plugins/firstorder/*
+plugins/fourier/*
+plugins/funind/*
+plugins/ltac/*
+plugins/micromega/*
+plugins/nsatz/*
+plugins/omega/*
+plugins/rtauto/*
+plugins/setoid/*
+plugins/ing/*
+plugins/setoid_ring/*
+plugins/ssr/*
+plugins/ssrmatching/*
+plugins/syntax/*
+# Enabled: none for now
diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md
index e26103cedd..1a12360c13 100644
--- a/CONTRIBUTING.md
+++ b/CONTRIBUTING.md
@@ -497,6 +497,11 @@ We have a linter that checks a few different things:
   your branch with `git rebase --whitespace=fix`.
 - **All files should end with a single newline**.  See the section
   [Style guide](#style-guide) for additional style recommendations.
+- **Code is properly formatted**: for some parts of the codebase,
+  formatting will be enforced using the
+  [`ocamlformat`](https://github.com/ocaml-ppx/ocamlformat) tool. You
+  can integrate the formatter in your editor of choice (see docs) or
+  use `dune build @fmt --auto-promote` to fix this kind of errors.
 
 You may run the linter yourself with `dev/lint-repository.sh`.
 
diff --git a/dev/doc/README.md b/dev/doc/README.md
index bc281e0d94..ba53605b0e 100644
--- a/dev/doc/README.md
+++ b/dev/doc/README.md
@@ -43,8 +43,12 @@ To learn how to run the test suite, you can read
 
 
 ## Development environment + tooling
+
 - [`Merlin`](https://github.com/ocaml/merlin) for autocomplete.
 - [Wiki pages on tooling containing `emacs`, `vim`, and `git` information](https://github.com/coq/coq/wiki/DevelSetup)
+- [`ocamlformat`](https://github.com/ocaml-ppx/ocamlformat) provides
+  support for automatic formatting of OCaml code. To use it please run
+  `dune build @fmt`, see `ocamlformat`'s documentation for more help.
 
 ## A note about rlwrap
 
diff --git a/dev/lint-repository.sh b/dev/lint-repository.sh
index 2e8a7455de..224601bbce 100755
--- a/dev/lint-repository.sh
+++ b/dev/lint-repository.sh
@@ -32,4 +32,7 @@ find . "(" -path ./.git -prune ")" -o -type f -print0 |
 echo Checking overlays
 dev/tools/check-overlays.sh || CODE=1
 
+echo Checking ocamlformat
+dune build @fmt || CODE=1
+
 exit $CODE
diff --git a/dune-project b/dune-project
index 1249c4af9f..fa05f5fb41 100644
--- a/dune-project
+++ b/dune-project
@@ -2,6 +2,9 @@
 (name coq)
 (using coq 0.1)
 
+(formatting
+ (enabled_for ocaml))
+
 ; We cannot set this to true until as long as the build is not
 ; properly bootstrapped [that is, we remove the voboot target]
 ;