updating links to stdlib and cocorico

jmadiot · jmadiot · commit 96a7432ae10d · 2025-06-23T13:31:51.000+02:00
diff --git a/gen.js b/gen.js
@@ -41,11 +41,10 @@ function link_description(url) {
   if(m = url.match(/^https:\/\/github.com\/coq-contribs\/([^\/]*)\//))
     return `coq-contribs/${m[1]}`;
   let known_urls = [
-    ["coq's standard library", "https://coq.inria.fr/library"],
+    ["coq's standard library", "https://rocq-prover.org/doc/V9.0.0/stdlib"],
     ["mathcomp", "https://math-comp.github.io/"],
     ["mathcomp", "https://github.com/math-comp/"],
     ["coq-contribs", "https://github.com/coq-contribs"],
-    ["cocorico", "https://coq.inria.fr/cocorico/"],
   ];
   for (let p of known_urls) {
     if (url.match(p[1])) return p[0];
@@ -133,4 +132,6 @@ let page = fs.readFileSync('template.html', 'utf8')
   .replace(/(?<=var stats = ){}/, JSON.stringify(stats, null, 2).replace(/\n/g, '\n      '))
 ;
 
+page = "<!-- This file is automatically generated; please do not modify it manually. -->\n" + page;
+
 process.stdout.write(page);
diff --git a/index.html b/index.html
@@ -1,3 +1,4 @@
+<!-- This file is automatically generated; please do not modify it manually. -->
 <!DOCTYPE html>
 <html lang="en">
   <head>
@@ -236,7 +237,7 @@ <h3 id='11' class='formalized'><a href='http://www.cs.ru.nl/~freek/100/#11'>11.
 <div>
 
 <p class='author'><strong>Russell O&#039;Connor</strong>
-  (in <a href="https://coq.inria.fr/cocorico/NotFinitePrimes">cocorico</a>):
+  (in <a href="https://web.archive.org/web/20151210214004/coq.inria.fr/cocorico/NotFinitePrimes">https://web.archive.org/web/20151210214004/coq.inria.fr/cocorico/NotFinitePrimes</a>):
 </p>
 <p class='comment'>This statement was formerly in cocorico, compatible with Coq 7.3</p>
 <pre class='statement'>Theorem ManyPrimes : ~(EX l:(list Prime) | (p:Prime)(In p l)).
@@ -321,7 +322,7 @@ <h3 id='15' class='formalized'><a href='http://www.cs.ru.nl/~freek/100/#15'>15.
 <p class='axioms'>Axioms used: (none)</p>
 
 <p class='author'><strong>The Coq development team</strong>
-  (in <a href="https://coq.inria.fr/library/Coq.Reals.RiemannInt.html">coq's standard library</a>):
+  (in <a href="https://rocq-prover.org/doc/V9.0.0/stdlib/Stdlib.Reals.RiemannInt.html">coq's standard library</a>):
 </p>
 <p class='comment'></p>
 <pre class='statement'>Lemma FTC_Riemann :
@@ -539,7 +540,7 @@ <h3 id='26' class='formalized'><a href='http://www.cs.ru.nl/~freek/100/#26'>26.
 <div>
 
 <p class='author'><strong>Guillaume Allais</strong>
-  (in <a href="https://coq.inria.fr/library/Coq.Reals.Ratan.html">coq's standard library</a>):
+  (in <a href="https://rocq-prover.org/doc/V9.0.0/stdlib/Stdlib.Reals.Ratan.html">coq's standard library</a>):
 </p>
 <p class='comment'></p>
 <pre class='statement'>Lemma PI_2_aux : {z : R | 7 / 8 &lt;= z &lt;= 7 / 4 /\ - cos z = 0}.
@@ -936,7 +937,7 @@ <h3 id='44' class='formalized'><a href='http://www.cs.ru.nl/~freek/100/#44'>44.
 <div>
 
 <p class='author'><strong>The Coq development team</strong>
-  (in <a href="https://coq.inria.fr/library/Coq.Reals.Binomial.html">coq's standard library</a>):
+  (in <a href="https://rocq-prover.org/doc/V9.0.0/stdlib/Stdlib.Reals.Binomial.html">coq's standard library</a>):
 </p>
 <p class='comment'>For the non-constructive type R</p>
 <pre class='statement'>Lemma binomial :
@@ -1241,7 +1242,7 @@ <h3 id='60' class='formalized'><a href='http://www.cs.ru.nl/~freek/100/#60'>60.
 <div>
 
 <p class='author'><strong>The Coq development team</strong>
-  (in <a href="https://coq.inria.fr/library/Coq.ZArith.Znumtheory.html">coq's standard library</a>):
+  (in <a href="https://rocq-prover.org/doc/V9.0.0/stdlib/Stdlib.ZArith.Znumtheory.html">coq's standard library</a>):
 </p>
 <p class='comment'></p>
 <pre class='statement'>Inductive Zdivide (a b:Z) : Prop :=
@@ -1377,7 +1378,7 @@ <h3 id='63' class='formalized'><a href='http://www.cs.ru.nl/~freek/100/#63'>63.
 <div>
 
 <p class='author'><strong>Gilles Kahn, Gerard Huet</strong>
-  (in <a href="https://coq.inria.fr/library/Coq.Sets.Powerset.html">coq's standard library</a>):
+  (in <a href="https://rocq-prover.org/doc/V9.0.0/stdlib/Stdlib.Sets.Powerset.html">coq's standard library</a>):
 </p>
 <p class='comment'>Naive Set Theory in Coq</p>
 <pre class='statement'>Theorem Strict_Rel_is_Strict_Included :
@@ -1518,7 +1519,7 @@ <h3 id='69' class='formalized'><a href='http://www.cs.ru.nl/~freek/100/#69'>69.
 <div>
 
 <p class='author'><strong>The Coq development team</strong>
-  (in <a href="https://coq.inria.fr/library/Coq.ZArith.Znumtheory.html">coq's standard library</a>):
+  (in <a href="https://rocq-prover.org/doc/V9.0.0/stdlib/Stdlib.ZArith.Znumtheory.html">coq's standard library</a>):
 </p>
 <p class='comment'>The following statement handle binary integers; other types are handled in the same file.</p>
 <pre class='statement'>Fixpoint Pgcdn (n: nat) (a b : positive) : positive :=
@@ -1630,7 +1631,7 @@ <h3 id='74' class='formalized'><a href='http://www.cs.ru.nl/~freek/100/#74'>74.
 <div>
 
 <p class='author'><strong>Coq&#039;s type theory</strong>
-  (in <a href="https://coq.inria.fr/library/Coq.Init.Datatypes.html">coq's standard library</a>):
+  (in <a href="https://rocq-prover.org/doc/V9.0.0/stdlib/Stdlib.Init.Datatypes.html">coq's standard library</a>):
 </p>
 <p class='comment'>The induction principle is automatically provided by Coq when defining unary natural numbers.</p>
 <pre class='statement'>Inductive nat : Set :=  O : nat | S : nat -&gt; nat.
@@ -1646,7 +1647,7 @@ <h3 id='74' class='formalized'><a href='http://www.cs.ru.nl/~freek/100/#74'>74.
 <p class='axioms'>Axioms used: (none)</p>
 
 <p class='author'><strong>The Coq development team</strong>
-  (in <a href="https://coq.inria.fr/library/Coq.NArith.BinNat.html#N.peano_rect">coq's standard library</a>):
+  (in <a href="https://rocq-prover.org/doc/V9.0.0/stdlib/Stdlib.NArith.BinNat.html#N.peano_rect">coq's standard library</a>):
 </p>
 <p class='comment'>Peano's induction principle is manually proved for binary natural integers.</p>
 <pre class='statement'>peano_rect : forall (P : N -&gt; Type),
@@ -1729,7 +1730,7 @@ <h3 id='79' class='formalized'><a href='http://www.cs.ru.nl/~freek/100/#79'>79.
 <div>
 
 <p class='author'><strong>The Coq development team</strong>
-  (in <a href="https://coq.inria.fr/library/Coq.Reals.Rsqrt_def.html">coq's standard library</a>):
+  (in <a href="https://rocq-prover.org/doc/V9.0.0/stdlib/Stdlib.Reals.Rsqrt_def.html">coq's standard library</a>):
 </p>
 <p class='comment'>non constructive version in Coq's standard library</p>
 <pre class='statement'>Lemma IVT_cor :
diff --git a/statements.yml b/statements.yml
@@ -133,7 +133,7 @@
 
 - theorem: 11
   authors: Russell O'Connor
-  link: https://coq.inria.fr/cocorico/NotFinitePrimes
+  link: https://web.archive.org/web/20151210214004/coq.inria.fr/cocorico/NotFinitePrimes
   comment: This statement was formerly in cocorico, compatible with Coq 7.3
   statement: |
     Theorem ManyPrimes : ~(EX l:(list Prime) | (p:Prime)(In p l)).
@@ -194,7 +194,7 @@
 
 - theorem: 15
   authors: The Coq development team
-  link: https://coq.inria.fr/library/Coq.Reals.RiemannInt.html
+  link: https://rocq-prover.org/doc/V9.0.0/stdlib/Stdlib.Reals.RiemannInt.html
   statement: |
     Lemma FTC_Riemann :
       forall (f:C1_fun) (a b:R) (pr:Riemann_integrable (derive f (diff0 f)) a b),
@@ -347,7 +347,7 @@
 
 - theorem: 26
   authors: Guillaume Allais
-  link: https://coq.inria.fr/library/Coq.Reals.Ratan.html
+  link: https://rocq-prover.org/doc/V9.0.0/stdlib/Stdlib.Reals.Ratan.html
   statement: |
     Lemma PI_2_aux : {z : R | 7 / 8 <= z <= 7 / 4 /\ - cos z = 0}.
     Definition PI := 2 * proj1_sig PI_2_aux.
@@ -636,7 +636,7 @@
 
 - theorem: 44
   authors: The Coq development team
-  link: https://coq.inria.fr/library/Coq.Reals.Binomial.html
+  link: https://rocq-prover.org/doc/V9.0.0/stdlib/Stdlib.Reals.Binomial.html
   comment: For the non-constructive type R
   statement: |
     Lemma binomial :
@@ -860,7 +860,7 @@
 
 - theorem: 60
   authors: The Coq development team
-  link: https://coq.inria.fr/library/Coq.ZArith.Znumtheory.html
+  link: https://rocq-prover.org/doc/V9.0.0/stdlib/Stdlib.ZArith.Znumtheory.html
   statement: |
     Inductive Zdivide (a b:Z) : Prop :=
       Zdivide_intro : forall q:Z, b = q * a -> Zdivide a b.
@@ -978,7 +978,7 @@
 
 - theorem: 63
   authors: Gilles Kahn, Gerard Huet
-  link: https://coq.inria.fr/library/Coq.Sets.Powerset.html
+  link: https://rocq-prover.org/doc/V9.0.0/stdlib/Stdlib.Sets.Powerset.html
   comment: Naive Set Theory in Coq
   statement: |
     Theorem Strict_Rel_is_Strict_Included :
@@ -1081,7 +1081,7 @@
 
 - theorem: 69
   authors: The Coq development team
-  link: https://coq.inria.fr/library/Coq.ZArith.Znumtheory.html
+  link: https://rocq-prover.org/doc/V9.0.0/stdlib/Stdlib.ZArith.Znumtheory.html
   comment: The following statement handle binary integers; other types are handled in the same file.
   statement: |
     Fixpoint Pgcdn (n: nat) (a b : positive) : positive :=
@@ -1170,7 +1170,7 @@
 
 - theorem: 74
   authors: Coq's type theory
-  link: https://coq.inria.fr/library/Coq.Init.Datatypes.html
+  link: https://rocq-prover.org/doc/V9.0.0/stdlib/Stdlib.Init.Datatypes.html
   comment: The induction principle is automatically provided by Coq when defining unary natural numbers.
   statement: |
     Inductive nat : Set :=  O : nat | S : nat -> nat.
@@ -1186,7 +1186,7 @@
 
 - theorem: 74
   authors: The Coq development team
-  link: https://coq.inria.fr/library/Coq.NArith.BinNat.html#N.peano_rect
+  link: https://rocq-prover.org/doc/V9.0.0/stdlib/Stdlib.NArith.BinNat.html#N.peano_rect
   comment: Peano's induction principle is manually proved for binary natural integers.
   statement: |
     peano_rect : forall (P : N -> Type),
@@ -1242,7 +1242,7 @@
 
 - theorem: 79
   authors: The Coq development team
-  link: https://coq.inria.fr/library/Coq.Reals.Rsqrt_def.html
+  link: https://rocq-prover.org/doc/V9.0.0/stdlib/Stdlib.Reals.Rsqrt_def.html
   comment: non constructive version in Coq's standard library
   statement: |
     Lemma IVT_cor :
