diff --git a/.gitignore b/.gitignore
index a99e667dc2348fa7daf75cfa1b382ee6daab59c4..6739522d9ebbda34e9600cde95de35e626360aec 100644
--- a/.gitignore
+++ b/.gitignore
@@ -116,11 +116,6 @@ autom4te.cache
 /doc/code/print_api/dynamic_plugins.mli
 /doc/code/print_api/_build/
 
-/doc/code/builtin
-/doc/code/studia
-/doc/code/qed
-/doc/code/wp
-
 /doc/developer/tutorial/viewcfg/src/META.frama-c-viewcfg
 /doc/developer/tutorial/viewcfg/src/Makefile
 /doc/developer/tutorial/viewcfg/src/gui/
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 4c5bc87370c3d80ca493fd151351f784533de44a..3661466d0917085a1a23043c43d51072442a2891 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -149,6 +149,14 @@ build-from-distrib-tarball:
   tags:
    - nix
 
+doc:
+  stage: tests
+  script:
+   - nix/frama-ci.sh build -A frama-c.doc
+  tags:
+   - nix
+  allow_failure: true
+
 .build_template: &internal_template
   stage: distrib_and_compatibility
   tags:
diff --git a/Makefile b/Makefile
index e47fd7c21ab188d1f178b5e6cb85f53130af2131..92ef5cef19d044f71cc5fc75009be091bc127b3d 100644
--- a/Makefile
+++ b/Makefile
@@ -1211,7 +1211,7 @@ FILES_FOR_OCAMLDEP+= $(addsuffix /*.mli,$(FRAMAC_SRC_DIRS)) \
 
 MODULES_TODOC+=$(filter-out $(MODULES_NODOC),\
 	$(MLI_ONLY) \
-	$(filter-out $(PLUGIN_TYPES_CMO_LIST:.cmo=.mli),$(CMO:.cmo=.mli))))
+	$(filter-out $(PLUGIN_TYPES_CMO_LIST:.cmo=.mli),$(CMO:.cmo=.mli)))
 
 ################################
 # toplevel.{byte,opt} binaries #
diff --git a/doc/code/.gitignore b/doc/code/.gitignore
index 8fe76cbf5c38b74c255641dfcec33d154b838dbd..94c6462e29b7c1ae8f0f29bad20a50c96e91a183 100644
--- a/doc/code/.gitignore
+++ b/doc/code/.gitignore
@@ -25,12 +25,15 @@
 /pdg/
 /postdominators/
 /print_api/
+/qed/
+/reduc/
 /report/
 /rte/
 /scope/
 /security_slicing/
 /slicing/
 /sparecode/
+/studia/
 /users/
 /value/
 /variadic/
diff --git a/nix/default.nix b/nix/default.nix
index 06da4832ca7f1f5474f2181bcfe1fd6e3a520059..fb7bbc39f54dd5971f8d681234840499737b1c55 100644
--- a/nix/default.nix
+++ b/nix/default.nix
@@ -112,6 +112,26 @@ pkgs.lib.makeExtensible
         '';
   };
 
+  doc = mk_deriv {
+        name = "frama-c-doc";
+        buildInputs = self.buildInputs;
+        build_dir = self.main.build_dir;
+        src = self.main.build_dir + "/dir.tar";
+        sourceRoot = ".";
+        postPatch = ''
+               find . \( -name "Makefile*" -or -name ".depend" -o -name "ptests_config" -o -name "config.status" \) -exec bash -c "t=\$(stat -c %y \"\$0\"); sed -i -e \"s&$(cat $build_dir/old_pwd)&$(pwd)&g\" \"\$0\"; touch -d \"\$t\" \"\$0\"" {} \;
+        '';
+        configurePhase = ''
+          true
+        '';
+        buildPhase = ''
+               make doc
+        '';
+        installPhase = ''
+               true
+        '';
+  } // { other-opam-selection = "main";};
+
   tests = mk_deriv {
         name = "frama-c-test";
         buildInputs = self.buildInputs;
diff --git a/src/kernel_services/abstract_interp/multidim.mli b/src/kernel_services/abstract_interp/multidim.mli
index 26ff49c7a5461a98469996db59c52a0a8245081d..e1d0a7dc839f2648bdc93427c6712448b2b1b33b 100644
--- a/src/kernel_services/abstract_interp/multidim.mli
+++ b/src/kernel_services/abstract_interp/multidim.mli
@@ -28,7 +28,7 @@
 
     or, more formally
 
-    { o + Σ dᵢ×xᵢ | ∀i 1≤i≤n ⇒ xᵢ ∊ [0, bᵢ] }
+    \{ o + Σ dᵢ×xᵢ | ∀i 1≤i≤n ⇒ xᵢ ∊ [0, bᵢ] \}
 
     This is a generalisation of integers intervals with modulo implemented in
     Ival : o + d×[0, b]