From 5acf32f58bade08442b5ba6395713233cc32786f Mon Sep 17 00:00:00 2001
From: Vincent Lafeychine <vincent.lafeychine@proton.me>
Date: Sat, 28 Sep 2024 22:06:26 +0200
Subject: [PATCH] Use specific version of Coq (8.20) for documentation
---
rr_frontend/radium/src/coq/eval_new.rs | 4 ++--
rr_frontend/radium/src/coq/mod.rs | 18 +++++++++---------
rr_frontend/radium/src/coq/module.rs | 2 +-
rr_frontend/radium/src/coq/module_new.rs | 6 +++---
rr_frontend/radium/src/coq/section.rs | 2 +-
rr_frontend/radium/src/coq/syntax_new.rs | 4 ++--
rr_frontend/radium/src/coq/term_new.rs | 6 +++---
7 files changed, 21 insertions(+), 21 deletions(-)
diff --git a/rr_frontend/radium/src/coq/eval_new.rs b/rr_frontend/radium/src/coq/eval_new.rs
index 7c7a3c6..9b5b6d9 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 04e0f7f..d0641f0 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 ed9cc5a..3304bff 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 9794979..35e731a 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 e2d76bf..09df08b 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 008fff6..310b84d 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 1d05534..b96af2e 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)]
--
GitLab