diff --git a/rr_frontend/Cargo.toml b/rr_frontend/Cargo.toml
index e3d002b894ebf638319f88b6e0dc5ed0b46e95db..ec8d9f9ef3c27a60c28706a6e911fe5a51bda4bf 100644
--- a/rr_frontend/Cargo.toml
+++ b/rr_frontend/Cargo.toml
@@ -21,7 +21,7 @@ analysis = { git = "https://github.com/viperproject/prusti-dev.git", rev = "24bd
 config = { version = "0.14", default-features = false, features = ["toml"] }
 csv = "1"
 datafrog = "2"
-derive_more = { version = "1.0.0-beta.6", features = ["display", "constructor", "debug"] }
+derive_more = { version = "1.0.0-beta.6", features = ["constructor", "debug", "deref", "display"] }
 env_logger = { version = "0.11" }
 glob = "0.3"
 indent_write = "2"
diff --git a/rr_frontend/radium/src/coq/mod.rs b/rr_frontend/radium/src/coq/mod.rs
index f24104c7edbb8affb71ec8132a80b6a1a737ed6d..4ada12f13703ce103361592702cfba3bf0b93563 100644
--- a/rr_frontend/radium/src/coq/mod.rs
+++ b/rr_frontend/radium/src/coq/mod.rs
@@ -4,10 +4,16 @@
 // If a copy of the BSD-3-clause license was not distributed with this
 // file, You can obtain one at https://opensource.org/license/bsd-3-clause/.
 
-/// A collection of types to represent and generate Rocq code.
+/// A collection of types to represent and generate [Rocq] code.
 ///
-/// These types are intended to be used for the purposes of this project.
+/// These types are intended to be used for the purposes of the [RefinedRust project].
 /// As such, they may not be suitable for general use.
+///
+/// This crate is split up in the same way as the [Rocq reference documentation].
+///
+/// [RefinedRust project]: https://plv.mpi-sws.org/refinedrust/
+/// [Rocq]: https://coq.inria.fr
+/// [Rocq reference]: https://coq.inria.fr/doc/master/refman/index.html
 pub mod command;
 pub mod module;
 pub mod term;
diff --git a/rr_frontend/radium/src/coq/module.rs b/rr_frontend/radium/src/coq/module.rs
index d986f808616dcf570d484493957a81b12ffd6f9d..d4483211015cba2f355870f19fa5f9445cd0382e 100644
--- a/rr_frontend/radium/src/coq/module.rs
+++ b/rr_frontend/radium/src/coq/module.rs
@@ -4,13 +4,14 @@
 // If a copy of the BSD-3-clause license was not distributed with this
 // file, You can obtain one at https://opensource.org/license/bsd-3-clause/.
 
-/// Rocq module system.
+/// The [module system].
+///
+/// [module system]: https://coq.inria.fr/doc/master/refman/language/core/modules.html
 use std::fmt;
-use std::ops::Deref;
 
-use derive_more::Display;
+use derive_more::{Deref, Display};
 
-/// A Rocq path of the form `A.B.C`.
+/// A path of the form `A.B.C`.
 #[derive(Clone, Eq, PartialEq, Hash, Debug, Display)]
 #[display("{}", _0)]
 pub struct Path(String);
@@ -27,7 +28,7 @@ impl Path {
     }
 }
 
-/// A Rocq module that contains a path `A.B.C` and a module name `D`.
+/// A module that contains a path `A.B.C` and a module name `D`.
 #[derive(Clone, Eq, PartialEq, Hash, Debug)]
 pub struct Module {
     path: Option<Path>,
@@ -57,10 +58,10 @@ impl Module {
     }
 }
 
-/// A Rocq import of the form `From A.B.C Require Import D`.
+/// An import of the form `From A.B.C Require Import D`.
 ///
 /// If the `path` is empty, it is of the form `Require Import A`.
-#[derive(Clone, Eq, PartialEq, Hash, Debug)]
+#[derive(Clone, Eq, PartialEq, Hash, Debug, Deref)]
 pub struct Import(Module);
 
 impl Import {
@@ -70,18 +71,10 @@ impl Import {
     }
 }
 
-impl Deref for Import {
-    type Target = Module;
-
-    fn deref(&self) -> &Self::Target {
-        &self.0
-    }
-}
-
-/// A Rocq export of the form `From A.B.C Require Export D`.
+/// An export of the form `From A.B.C Require Export D`.
 ///
 /// If the `path` is empty, it is of the form `Require Export A`.
-#[derive(Clone, Eq, PartialEq, Hash, Debug)]
+#[derive(Clone, Eq, PartialEq, Hash, Debug, Deref)]
 pub struct Export(Module);
 
 impl Export {
@@ -91,14 +84,7 @@ impl Export {
     }
 }
 
-impl Deref for Export {
-    type Target = Module;
-
-    fn deref(&self) -> &Self::Target {
-        &self.0
-    }
-}
-
+/// Get every unique path from a list of modules.
 fn get_modules_path(modules: &[&Module]) -> Vec<Path> {
     let paths: Vec<_> = modules.iter().filter_map(|x| x.get_path()).collect();
 
@@ -111,6 +97,7 @@ fn get_modules_path(modules: &[&Module]) -> Vec<Path> {
     result
 }
 
+/// Pretty printing a list of modules, by merging the ones with the same path.
 fn fmt_modules(f: &mut fmt::Formatter<'_>, modules: &[&Module], kind: &str) -> fmt::Result {
     fn is(module: &Module, path: Option<&Path>) -> Option<String> {
         (module.get_path() == path.cloned()).then(|| module.name.clone())