diff --git a/.gitignore b/.gitignore
index 847c638f8dd074bf3e81c121ca2cec2435d5ed9e..76f29b1cd1cb24d6052be66d011b6e49996440ad 100644
--- a/.gitignore
+++ b/.gitignore
@@ -22,3 +22,5 @@ Makefile.package.*
 html/
 builddep/
 _opam
+_build/
+*.install
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 74782b10333668285a330ee92c17df20929cc7a0..48b28040516af86240fc729991a18202ede41ae5 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -67,6 +67,14 @@ build-coq.8.19.0-mr:
     DENY_WARNINGS: "1"
     MANGLE_NAMES: "1"
 
+# Also ensure Dune works.
+build-coq.8.19.0-dune:
+  <<: *template
+  <<: *branches_and_mr
+  variables:
+    OPAM_PINS: "coq version 8.19.0 dune   version 3.15.2"
+    MAKE_TARGET: "dune"
+
 # The oldest version runs in MRs, without name mangling.
 build-coq.8.18.0:
   <<: *template
diff --git a/CHANGELOG.md b/CHANGELOG.md
index 68701b609a437bd2f937781ffa9df527b641cd2b..5de5b3039768271ecdb68350603c5dd3fb617c52 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -7,6 +7,7 @@ API-breaking change is listed.
   `gmultiset_set_fold_comm_acc` to have more general type. (by Yannick Zakowski)
 - Strengthen `map_disjoint_difference_l` and `map_disjoint_difference_l`, and
   thereby make them consistent with the corresponding lemmas for sets.
+- Allow compiling the packages with dune (!552, by Rodolphe Lepigre).
 
 ## std++ 1.10.0 (2024-04-12)
 
diff --git a/Makefile b/Makefile
index ac8dba01d935c2dbd09966a33cc7afa229b68cfa..c837f883f58cacd6ee79b86a3a1170702571d75f 100644
--- a/Makefile
+++ b/Makefile
@@ -3,6 +3,12 @@ all: Makefile.coq
 	+@$(MAKE) -f Makefile.coq all
 .PHONY: all
 
+# Build with dune.
+# This exists only for CI; you should just call `dune build` directly instead.
+dune:
+	@dune build --display=short
+.PHONY: dune
+
 # Permit local customization
 -include Makefile.local
 
diff --git a/docs/dune.md b/docs/dune.md
new file mode 100644
index 0000000000000000000000000000000000000000..e45a0a3f11fcf21e30c508eb99aa53e6ff25bd82
--- /dev/null
+++ b/docs/dune.md
@@ -0,0 +1,45 @@
+Support for the dune build system
+=================================
+
+**NOTE:** in case of problem with the dune build, you can ask @lepigre or
+@Blaisorblade for help.
+
+The library can be built using dune by running `dune build`. Note that `dune`
+needs to be installed separately with `opam install dune`, as it is currently
+not part of the dependencies of the project.
+
+Useful links:
+- [dune documentation](https://dune.readthedocs.io)
+- [coq zulip channel](https://coq.zulipchat.com/#narrow/stream/240550-Dune-devs-.26-users)
+
+
+Editor support
+--------------
+
+Good dune support in editors is lacking at the moment, but there are trick you
+can play to make it work.
+
+One option is to configure your editor to invoke the `dune coq top` command
+instead of `coqtop`, but that is not easy to configure.
+
+Another option is to change the `_CoqProject` file to something like:
+```
+-Q stdpp stdpp
+-Q _build/default/stdpp stdpp
+-Q stdpp_bitvector stdpp.bitvector
+-Q _build/default/stdpp_bitvector stdpp.bitvector
+-Q stdpp_unstable stdpp.unstable
+-Q _build/default/stdpp_unstable stdpp.unstable
+```
+Note that this includes two bindings for each logical path: a binding to a
+folder in the source tree (where editors will find the `.v` files), and a
+binding to the same folder under `_build/default` (where editors will find
+the corresponding `.vo` files). The binding for a source folder must come
+before the binding for the corresponding build folder, so that editors know
+to jump to source files in the source tree (and not their read-only copy in
+the build folder).
+
+If you do this, you still need to invoke `dune` manually to make sure that the
+dependencies of the file you are stepping through are up-to-date. To build a
+single file, you can do, e.g., `dune build stdpp/options.vo`. To build only
+the `stdpp` folder, you can do `dune build stdpp`.
diff --git a/dune b/dune
new file mode 100644
index 0000000000000000000000000000000000000000..822f87d0b104c5fc69a8aca77c3b812a5b42f27c
--- /dev/null
+++ b/dune
@@ -0,0 +1,7 @@
+(env
+ (_ ; Applies to all profiles (dev, release, ...).
+  (coq
+   (flags ; Configure the coqc flags.
+    (:standard ; Keeping the default flags.
+     ; Add custom flags (to be kept in sync with _CoqProject).
+     -w -argument-scope-delimiter)))))
diff --git a/dune-project b/dune-project
new file mode 100644
index 0000000000000000000000000000000000000000..8b858cdefd7c9d75074c1113a19f4476bd2bb89f
--- /dev/null
+++ b/dune-project
@@ -0,0 +1,2 @@
+(lang dune 3.8)
+(using coq 0.8)
diff --git a/stdpp/dune b/stdpp/dune
new file mode 100644
index 0000000000000000000000000000000000000000..d9ff07ded50d2d5d62dd1e5a7812117d6f7f08be
--- /dev/null
+++ b/stdpp/dune
@@ -0,0 +1,4 @@
+(include_subdirs qualified)
+(coq.theory
+ (name stdpp)
+ (package coq-stdpp))
diff --git a/stdpp_bitvector/dune b/stdpp_bitvector/dune
new file mode 100644
index 0000000000000000000000000000000000000000..c088d18222183d073d0009fb335ed55dcb724b86
--- /dev/null
+++ b/stdpp_bitvector/dune
@@ -0,0 +1,5 @@
+(include_subdirs qualified)
+(coq.theory
+ (name stdpp.bitvector)
+ (package coq-stdpp-bitvector)
+ (theories stdpp))
diff --git a/stdpp_unstable/dune b/stdpp_unstable/dune
new file mode 100644
index 0000000000000000000000000000000000000000..0c360b623c6227664038dd27f62e2b5b629e5440
--- /dev/null
+++ b/stdpp_unstable/dune
@@ -0,0 +1,5 @@
+(include_subdirs qualified)
+(coq.theory
+ (name stdpp.unstable)
+ (package coq-stdpp-unstable)
+ (theories stdpp stdpp.bitvector))