diff --git a/rr_frontend/Cargo.toml b/rr_frontend/Cargo.toml
index fe1903586565a5c8eb8af2a7a60c4dd8b681dbd6..f4de0a297bdbf8fa55dfa994069100ad6ef24dbb 100644
--- a/rr_frontend/Cargo.toml
+++ b/rr_frontend/Cargo.toml
@@ -22,7 +22,7 @@ config = { version = "0.14", default-features = false, features = ["toml"] }
 csv = "1"
 datafrog = "2"
 derive-new = "0.5"
-derive_more = { version = "1.0.0-beta.6", features = ["constructor", "debug", "deref", "deref_mut", "display"] }
+derive_more = { version = "1.0.0-beta.6", features = ["constructor", "debug", "deref", "deref_mut", "display", "from"] }
 env_logger = { version = "0.11" }
 from_variants = "1"
 glob = "0.3"
diff --git a/rr_frontend/radium/src/coq/command_new/compiled_files.rs b/rr_frontend/radium/src/coq/command_new/compiled_files.rs
new file mode 100644
index 0000000000000000000000000000000000000000..34432f3a60e65f106c9275d6e1a79ccc1a9a93d6
--- /dev/null
+++ b/rr_frontend/radium/src/coq/command_new/compiled_files.rs
@@ -0,0 +1,53 @@
+// © 2023, The RefinedRust Developers and Contributors
+//
+// This Source Code Form is subject to the terms of the BSD-3-clause License.
+// 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/.
+
+use std::fmt;
+
+/// A [dirpath].
+///
+/// [dirpath]: https://coq.inria.fr/doc/master/refman/proof-engine/vernacular-commands.html#grammar-token-dirpath
+#[derive(Clone, Eq, PartialEq, Debug)]
+pub struct DirPath(Vec<String>);
+
+/// Either an Import or an Export flag.
+#[derive(Clone, Eq, PartialEq, Debug)]
+pub enum Kind {
+    Import,
+    Export,
+}
+
+/// A [`From ... Require`] command.
+///
+/// [`From ... Require`]: https://coq.inria.fr/doc/master/refman/proof-engine/vernacular-commands.html#coq:cmd.From-%E2%80%A6-Require
+#[derive(Clone, Eq, PartialEq, Debug)]
+pub struct FromRequire {
+    pub from: Option<String>,
+    pub import: Vec<String>,
+    pub kind: Kind,
+}
+
+impl FromRequire {
+    #[must_use]
+    pub fn new(import: Vec<impl Into<String>>, kind: Kind) -> Self {
+        let from = None;
+        let import = import.into_iter().map(Into::into).collect();
+
+        Self { from, kind, import }
+    }
+
+    #[must_use]
+    pub fn from(self, from: impl Into<String>) -> Self {
+        let from = Some(from.into());
+
+        Self { from, ..self }
+    }
+}
+
+impl fmt::Display for FromRequire {
+    fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
+        write!(f, "")
+    }
+}
diff --git a/rr_frontend/radium/src/coq/command_new/mod.rs b/rr_frontend/radium/src/coq/command_new/mod.rs
new file mode 100644
index 0000000000000000000000000000000000000000..c0d4006d5c1e03389897c17d16f61c115f80358a
--- /dev/null
+++ b/rr_frontend/radium/src/coq/command_new/mod.rs
@@ -0,0 +1,58 @@
+// © 2023, The RefinedRust Developers and Contributors
+//
+// This Source Code Form is subject to the terms of the BSD-3-clause License.
+// 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/.
+
+pub mod compiled_files;
+
+use derive_more::Display;
+use from_variants::FromVariants;
+
+use crate::coq;
+use crate::coq::settings;
+
+/// A [command], with optional attributes.
+///
+/// [command]: https://coq.inria.fr/doc/master/refman/language/core/basic.html#grammar-token-command
+#[derive(Clone, Eq, PartialEq, Debug, Display)]
+#[display("{} {}.", command, attributes.as_ref().map_or(String::new(), |a| a.to_string()))]
+pub struct CommandAttrs {
+    pub command: Command,
+    pub attributes: Option<settings::Attribute>,
+}
+
+impl CommandAttrs {
+    #[must_use]
+    pub fn new(command: impl Into<Command>) -> Self {
+        Self {
+            attributes: None,
+            command: command.into(),
+        }
+    }
+
+    #[must_use]
+    pub fn attributes(self, attributes: impl Into<settings::Attribute>) -> Self {
+        let attributes = Some(attributes.into());
+
+        Self { attributes, ..self }
+    }
+}
+
+/// A [command].
+///
+/// [command]: https://coq.inria.fr/doc/master/refman/coq-cmdindex.html#command-index
+#[derive(Clone, Eq, PartialEq, Debug, Display, FromVariants)]
+pub enum Command {
+    #[display("{}", _0)]
+    FromRequire(compiled_files::FromRequire),
+
+    #[display("Proof")]
+    Proof,
+}
+
+impl From<Command> for coq::Sentence {
+    fn from(command: Command) -> Self {
+        Self::CommandAttrs(CommandAttrs::new(command))
+    }
+}
diff --git a/rr_frontend/radium/src/coq/mod.rs b/rr_frontend/radium/src/coq/mod.rs
index 6bc9590c55177761f5c4f46bbd48cc386a53a4db..d27f6fc1a3afcc722878d2bcd58f2f7c190d8c3c 100644
--- a/rr_frontend/radium/src/coq/mod.rs
+++ b/rr_frontend/radium/src/coq/mod.rs
@@ -295,24 +295,25 @@
 //! [sections]: https://coq.inria.fr/doc/master/refman/language/core/sections.html
 
 pub mod command;
+pub mod command_new;
 pub mod module;
+pub mod settings;
 pub mod term;
 
 use std::fmt;
 
-use derive_more::{Deref, DerefMut, Display};
+use derive_more::{Deref, DerefMut, Display, From};
 use derive_new::new;
 use from_variants::FromVariants;
 use indoc::writedoc;
 
-use crate::write_list;
+use crate::display_list;
 
-/// A [document] is the entry-point to create a script, composed of [sentences].
+/// A [document].
 ///
-/// [commands]: https://coq.inria.fr/doc/master/refman/language/core/basic.html#grammar-token-command
 /// [document]: https://coq.inria.fr/doc/master/refman/language/core/basic.html#grammar-token-document
-/// [sentences]: https://coq.inria.fr/doc/master/refman/language/core/basic.html#grammar-token-sentence
-#[derive(Eq, PartialEq, Debug, Default, Deref, DerefMut)]
+#[derive(Clone, Eq, PartialEq, Debug, Display, Default, Deref, DerefMut)]
+#[display("{}", display_list!(_0, "\n"))]
 pub struct Document(pub Vec<Sentence>);
 
 impl Document {
@@ -326,88 +327,34 @@ impl Document {
     }
 }
 
-/// Beware, imports and exports [Command] are gathered on top of the list.
-#[derive(Eq, PartialEq, Debug, FromVariants)]
-pub enum Sentence {
-    CommandAttrs(CommandAttrs),
-}
-
-#[derive(Eq, PartialEq, Debug)]
-pub struct CommandAttrs {
-    pub command: Command,
-    pub attributes: Option<String>,
-}
-
-impl CommandAttrs {
-    #[must_use]
-    pub fn new(command: impl Into<Command>) -> Self {
-        Self {
-            attributes: None,
-            command: command.into(),
-        }
-    }
-
-    #[must_use]
-    pub fn attributes(self, attributes: impl Into<String>) -> Self {
-        let attributes = Some(attributes.into());
-
-        Self { attributes, ..self }
-    }
-}
-
-/// A [command], the entrypoint of everything that can be written.
+/// A [sentence].
 ///
-/// [command]: https://coq.inria.fr/doc/master/refman/language/core/basic.html#grammar-token-command
-#[derive(Eq, PartialEq, Debug, FromVariants)]
-pub enum Command {
-    Require(Require),
-
-    Proof,
-    // TODO: Add section, ...
-}
-
-impl From<Command> for Sentence {
-    fn from(command: Command) -> Self {
-        Self::CommandAttrs(CommandAttrs::new(command))
-    }
-}
-
-#[derive(Eq, PartialEq, Debug)]
-pub struct Require {
-    pub from: Option<String>,
-    pub import: Vec<String>,
-}
-
-impl Require {
-    #[must_use]
-    pub fn new(import: Vec<impl Into<String>>) -> Self {
-        Self {
-            from: None,
-            import: import.into_iter().map(Into::into).collect(),
-        }
-    }
-
-    #[must_use]
-    pub fn from(self, from: impl Into<String>) -> Self {
-        let from = Some(from.into());
-
-        Self { from, ..self }
-    }
+/// [sentence]: https://coq.inria.fr/doc/master/refman/language/core/basic.html#grammar-token-sentence
+#[derive(Clone, Eq, PartialEq, Debug, Display, FromVariants)]
+pub enum Sentence {
+    #[display("{}", _0)]
+    CommandAttrs(command_new::CommandAttrs),
 }
 
 #[cfg(test)]
 mod tests {
+    use command_new::compiled_files::*;
+    use command_new::*;
+
     use super::*;
 
     #[test]
     fn test_document() {
         let mut doc = Document::new(vec![
-            Command::Require(Require::new(vec!["nat", "bool"]).from("Coq.Init.Datatypes")),
-            Command::Require(Require::new(vec!["nat", "bool"]).from("Coq.Init.Datatypes")),
+            Command::FromRequire(
+                FromRequire::new(vec!["nat", "bool"], Kind::Import).from("Coq.Init.Datatypes"),
+            ),
             Command::Proof,
         ]);
 
-        doc.push(Command::Require(Require::new(vec!["nat", "bool"]).from("Coq.Init.Datatypes")));
+        doc.push(Command::FromRequire(
+            FromRequire::new(vec!["nat", "bool"], Kind::Import).from("Coq.Init.Datatypes"),
+        ));
         doc.push(Command::Proof);
         doc.push(CommandAttrs::new(Command::Proof).attributes("Some"));
     }
diff --git a/rr_frontend/radium/src/coq/module.rs b/rr_frontend/radium/src/coq/module.rs
index d4483211015cba2f355870f19fa5f9445cd0382e..ed9cc5ae7da1db164d583446aa13bfd21c79984e 100644
--- a/rr_frontend/radium/src/coq/module.rs
+++ b/rr_frontend/radium/src/coq/module.rs
@@ -18,8 +18,8 @@ pub struct Path(String);
 
 impl Path {
     #[must_use]
-    pub fn new(path: &str) -> Self {
-        Self(path.to_owned())
+    pub fn new(path: impl Into<String>) -> Self {
+        Self(path.into())
     }
 
     #[must_use]
diff --git a/rr_frontend/radium/src/coq/section.rs b/rr_frontend/radium/src/coq/section.rs
new file mode 100644
index 0000000000000000000000000000000000000000..e2d76bf401908dee5c34f4cae64237b5d28d05d3
--- /dev/null
+++ b/rr_frontend/radium/src/coq/section.rs
@@ -0,0 +1,26 @@
+// © 2023, The RefinedRust Developers and Contributors
+//
+// This Source Code Form is subject to the terms of the BSD-3-clause License.
+// 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/.
+
+/// [Sections].
+///
+/// [Sections]: https://coq.inria.fr/doc/master/refman/language/core/sections.html
+use derive_more::Display;
+
+#[derive(Clone, Eq, PartialEq, Hash, Debug, Display)]
+#[display("Section {}", name)]
+pub struct Section {
+    name: String,
+}
+
+impl Section {
+    pub fn new(name: String) -> Self {
+        Self { name }
+    }
+
+    pub fn name(&self) -> &str {
+        &self.name
+    }
+}
diff --git a/rr_frontend/radium/src/coq/settings.rs b/rr_frontend/radium/src/coq/settings.rs
new file mode 100644
index 0000000000000000000000000000000000000000..4418527b5042877637c735ecdb7aa3db6b95cb0e
--- /dev/null
+++ b/rr_frontend/radium/src/coq/settings.rs
@@ -0,0 +1,19 @@
+// © 2023, The RefinedRust Developers and Contributors
+//
+// This Source Code Form is subject to the terms of the BSD-3-clause License.
+// 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/.
+
+//! Mechanisms, called [settings], for changing the behaviour of Rocq.
+//!
+//! [settings]: https://coq.inria.fr/doc/master/refman/language/core/basic.html#settings
+
+use derive_more::{Display, From};
+
+/// An [attribute].
+///
+/// [attribute]: https://coq.inria.fr/doc/master/refman/language/core/basic.html#grammar-token-attribute
+#[derive(Clone, Eq, PartialEq, Debug, Display, From)]
+#[from(forward)]
+#[display("{}", _0)]
+pub struct Attribute(String);