diff --git a/rr_frontend/radium/src/coq/eval_new.rs b/rr_frontend/radium/src/coq/eval_new.rs
index 7c7a3c6bb8bf9dc0c07e89803bdd38d3268bd20f..9b5b6d9321d88d90a38e460488e6c895919f1e6e 100644
--- a/rr_frontend/radium/src/coq/eval_new.rs
+++ b/rr_frontend/radium/src/coq/eval_new.rs
@@ -6,7 +6,7 @@
 
 //! The [eval] section. This module will be renamed `eval`.
 //!
-//! [eval]: https://coq.inria.fr/doc/master/refman/proofs/writing-proofs/equality.html#computing-in-a-term-eval-and-eval
+//! [eval]: https://coq.inria.fr/doc/v8.20/refman/proofs/writing-proofs/equality.html#computing-in-a-term-eval-and-eval
 
 use derive_more::{Deref, DerefMut, Display};
 
@@ -14,7 +14,7 @@ use crate::coq::term_new;
 
 /// The [`Compute`] command.
 ///
-/// [`Compute`]: https://coq.inria.fr/doc/master/refman/proofs/writing-proofs/equality.html#coq:cmd.Compute
+/// [`Compute`]: https://coq.inria.fr/doc/v8.20/refman/proofs/writing-proofs/equality.html#coq:cmd.Compute
 #[derive(Clone, Eq, PartialEq, Debug, Display, Deref, DerefMut)]
 #[display("Compute {}", _0)]
 pub struct Compute(pub term_new::Term);
diff --git a/rr_frontend/radium/src/coq/mod.rs b/rr_frontend/radium/src/coq/mod.rs
index 04e0f7ff27f03921b8f13c56f4ff5368d5a6691f..d0641f05a55a491366f46ea8738fc928edb50901 100644
--- a/rr_frontend/radium/src/coq/mod.rs
+++ b/rr_frontend/radium/src/coq/mod.rs
@@ -311,8 +311,8 @@
 //!
 //! [RefinedRust project]: https://plv.mpi-sws.org/refinedrust/
 //! [Rocq]: https://coq.inria.fr
-//! [Rocq reference]: https://coq.inria.fr/doc/master/refman/index.html
-//! [sections]: https://coq.inria.fr/doc/master/refman/language/core/sections.html
+//! [Rocq reference]: https://coq.inria.fr/doc/v8.20/refman/index.html
+//! [sections]: https://coq.inria.fr/doc/v8.20/refman/language/core/sections.html
 
 pub mod command;
 pub mod eval_new;
@@ -331,7 +331,7 @@ use crate::display_list;
 
 /// A [document].
 ///
-/// [document]: https://coq.inria.fr/doc/master/refman/language/core/basic.html#grammar-token-document
+/// [document]: https://coq.inria.fr/doc/v8.20/refman/language/core/basic.html#grammar-token-document
 #[derive(Clone, Eq, PartialEq, Debug, Display, Default, Deref, DerefMut)]
 #[display("{}\n", display_list!(_0, "\n"))]
 pub struct Document(pub Vec<Sentence>);
@@ -349,7 +349,7 @@ impl Document {
 
 /// A [sentence].
 ///
-/// [sentence]: https://coq.inria.fr/doc/master/refman/language/core/basic.html#grammar-token-sentence
+/// [sentence]: https://coq.inria.fr/doc/v8.20/refman/language/core/basic.html#grammar-token-sentence
 #[derive(Clone, Eq, PartialEq, Debug, Display, FromVariants)]
 pub enum Sentence {
     #[display("{}", _0)]
@@ -361,7 +361,7 @@ pub enum Sentence {
 
 /// A [command], with optional attributes.
 ///
-/// [command]: https://coq.inria.fr/doc/master/refman/language/core/basic.html#grammar-token-command
+/// [command]: https://coq.inria.fr/doc/v8.20/refman/language/core/basic.html#grammar-token-command
 #[derive(Clone, Eq, PartialEq, Debug)]
 pub struct CommandAttrs {
     pub command: Command,
@@ -397,7 +397,7 @@ impl CommandAttrs {
 
 /// A [command].
 ///
-/// [command]: https://coq.inria.fr/doc/master/refman/language/core/basic.html#grammar-token-command
+/// [command]: https://coq.inria.fr/doc/v8.20/refman/language/core/basic.html#grammar-token-command
 #[derive(Clone, Eq, PartialEq, Debug, Display, FromVariants)]
 pub enum Command {
     #[display("{}", _0)]
@@ -418,7 +418,7 @@ impl From<Command> for Sentence {
 
 /// A [query command], with optional attributes.
 ///
-/// [query command]: https://coq.inria.fr/doc/master/refman/proof-engine/vernacular-commands.html#grammar-token-query_command
+/// [query command]: https://coq.inria.fr/doc/v8.20/refman/proof-engine/vernacular-commands.html#grammar-token-query_command
 #[derive(Clone, Eq, PartialEq, Debug)]
 pub struct QueryCommandAttrs {
     pub command: QueryCommand,
@@ -460,7 +460,7 @@ impl QueryCommandAttrs {
 
 /// A [query command].
 ///
-/// [query command]: https://coq.inria.fr/doc/master/refman/proof-engine/vernacular-commands.html#grammar-token-query_command
+/// [query command]: https://coq.inria.fr/doc/v8.20/refman/proof-engine/vernacular-commands.html#grammar-token-query_command
 #[derive(Clone, Eq, PartialEq, Debug, Display, FromVariants)]
 pub enum QueryCommand {
     #[display("{}", _0)]
@@ -475,7 +475,7 @@ impl From<QueryCommand> for Sentence {
 
 /// An [attribute].
 ///
-/// [attribute]: https://coq.inria.fr/doc/master/refman/language/core/basic.html#grammar-token-attribute
+/// [attribute]: https://coq.inria.fr/doc/v8.20/refman/language/core/basic.html#grammar-token-attribute
 #[derive(Clone, Eq, PartialEq, Debug, Display, From)]
 #[from(forward)]
 #[display("{}", _0)]
diff --git a/rr_frontend/radium/src/coq/module.rs b/rr_frontend/radium/src/coq/module.rs
index ed9cc5ae7da1db164d583446aa13bfd21c79984e..3304bff08074d5fa82981a59a93d9e804269e4c5 100644
--- a/rr_frontend/radium/src/coq/module.rs
+++ b/rr_frontend/radium/src/coq/module.rs
@@ -6,7 +6,7 @@
 
 /// The [module system].
 ///
-/// [module system]: https://coq.inria.fr/doc/master/refman/language/core/modules.html
+/// [module system]: https://coq.inria.fr/doc/v8.20/refman/language/core/modules.html
 use std::fmt;
 
 use derive_more::{Deref, Display};
diff --git a/rr_frontend/radium/src/coq/module_new.rs b/rr_frontend/radium/src/coq/module_new.rs
index 97949795f83b1e72a9e02b6e77f3e9c159b9a075..35e731a0fd67277ff3c938a94e95d66b3857a395 100644
--- a/rr_frontend/radium/src/coq/module_new.rs
+++ b/rr_frontend/radium/src/coq/module_new.rs
@@ -6,7 +6,7 @@
 
 //! The [module] section. This module will be renamed `module`.
 //!
-//! [module]: https://coq.inria.fr/doc/master/refman/language/core/modules.html
+//! [module]: https://coq.inria.fr/doc/v8.20/refman/language/core/modules.html
 
 use std::fmt;
 
@@ -16,7 +16,7 @@ use crate::{display_list, write_list};
 
 /// A [dirpath].
 ///
-/// [dirpath]: https://coq.inria.fr/doc/master/refman/proof-engine/vernacular-commands.html#grammar-token-dirpath
+/// [dirpath]: https://coq.inria.fr/doc/v8.20/refman/proof-engine/vernacular-commands.html#grammar-token-dirpath
 #[derive(Clone, Eq, PartialEq, Debug, Display, Default, Deref, DerefMut)]
 #[display("{}", display_list!(_0, "."))]
 pub struct DirPath(pub Vec<String>);
@@ -36,7 +36,7 @@ pub enum Kind {
 
 /// The [`From ... Require`] command.
 ///
-/// [`From ... Require`]: https://coq.inria.fr/doc/master/refman/proof-engine/vernacular-commands.html#coq:cmd.From-%E2%80%A6-Require
+/// [`From ... Require`]: https://coq.inria.fr/doc/v8.20/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>,
diff --git a/rr_frontend/radium/src/coq/section.rs b/rr_frontend/radium/src/coq/section.rs
index e2d76bf401908dee5c34f4cae64237b5d28d05d3..09df08bb407860231e9d95a09dabd7f97b37ff83 100644
--- a/rr_frontend/radium/src/coq/section.rs
+++ b/rr_frontend/radium/src/coq/section.rs
@@ -6,7 +6,7 @@
 
 /// [Sections].
 ///
-/// [Sections]: https://coq.inria.fr/doc/master/refman/language/core/sections.html
+/// [Sections]: https://coq.inria.fr/doc/v8.20/refman/language/core/sections.html
 use derive_more::Display;
 
 #[derive(Clone, Eq, PartialEq, Hash, Debug, Display)]
diff --git a/rr_frontend/radium/src/coq/syntax_new.rs b/rr_frontend/radium/src/coq/syntax_new.rs
index 008fff6dceeeeafb84b277418eaeda58cc21d72e..310b84dcd566bdf959d58e5d704780e9e71f2f70 100644
--- a/rr_frontend/radium/src/coq/syntax_new.rs
+++ b/rr_frontend/radium/src/coq/syntax_new.rs
@@ -6,13 +6,13 @@
 
 //! The [syntax and notations] section. This module will be renamed `syntax`.
 //!
-//! [syntax and notations]: https://coq.inria.fr/doc/master/refman/user-extensions/syntax-extensions.html
+//! [syntax and notations]: https://coq.inria.fr/doc/v8.20/refman/user-extensions/syntax-extensions.html
 
 use derive_more::{Deref, DerefMut, Display, From};
 
 /// The [`Open Scope`] command.
 ///
-/// [`Open Scope`]: https://coq.inria.fr/doc/master/refman/user-extensions/syntax-extensions.html#coq:cmd.Open-Scope
+/// [`Open Scope`]: https://coq.inria.fr/doc/v8.20/refman/user-extensions/syntax-extensions.html#coq:cmd.Open-Scope
 #[derive(Clone, Eq, PartialEq, Debug, Display, Default, Deref, DerefMut, From)]
 #[from(forward)]
 #[display("Open Scope {}", _0)]
diff --git a/rr_frontend/radium/src/coq/term_new.rs b/rr_frontend/radium/src/coq/term_new.rs
index 1d055344ea7ab398d75b0edabd7d6bb9f6021257..b96af2e19f1c6c52a56a47486fa259b897e7e008 100644
--- a/rr_frontend/radium/src/coq/term_new.rs
+++ b/rr_frontend/radium/src/coq/term_new.rs
@@ -4,16 +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/.
 
-//! The [terms] section. This module will be renamed `term`.
+//! The [terms] section.
 //!
-//! [terms]: https://coq.inria.fr/doc/master/refman/language/core/basic.html#term-term
+//! [terms]: https://coq.inria.fr/doc/v8.20/refman/language/core/basic.html#term-term
 
 use derive_more::Display;
 use from_variants::FromVariants;
 
 /// A [term].
 ///
-/// [term]: https://coq.inria.fr/doc/master/refman/language/core/basic.html#grammar-token-term
+/// [term]: https://coq.inria.fr/doc/v8.20/refman/language/core/basic.html#grammar-token-term
 #[derive(Clone, Eq, PartialEq, Debug, Display, FromVariants)]
 pub enum Term {
     #[display("\"{}\"", _0)]