Merge pull request #224 from maximedenes/add-distrib-redirects

Stop relying on distrib reverse proxy

news/coq-8-12-2-is-out

@@ -10,7 +10,7 @@ href="https://github.com/coq/coq/releases/tag/V8.12.2">release of Coq
 
 <p>This release fixes two impacting 8.12 regressions (in notations and
 the implicit argument inference of the exists tactic).  See the <a
-href="https://coq.inria.fr/distrib/V8.12.2/refman/changes.html#changes-in-8-12-2">changelog</a>
+href="https://coq.github.io/doc/V8.12.2/refman/changes.html#changes-in-8-12-2">changelog</a>
 for details.</p>
 
 </#def>

news/coq-83-beta-version

@@ -3,7 +3,7 @@
 <#def AUTHOR>coq-www</#def>
 <#def DATE>16 Feb 2010 17:44 GMT</#def>
 <#def DESCR>
-<p>The Coq developpers are pleased to announce the release of the <em>beta</em> version of Coq 8.3. This release intends to give the curious and impatient users of Coq a flavour of what Coq 8.3 will be. To see what is new in this version of Coq, please refer to the <a href="/distrib/V8.3-beta0/CHANGES">CHANGES</a> file.</p>
+<p>The Coq developpers are pleased to announce the release of the <em>beta</em> version of Coq 8.3. This release intends to give the curious and impatient users of Coq a flavour of what Coq 8.3 will be. To see what is new in this version of Coq, please refer to the <a href="https://coq-distrib.s3-website.fr-par.scw.cloud/V8.3-beta0/CHANGES">CHANGES</a> file.</p>
 <p>Please be aware that this release should be considered as <strong>unstable</strong>, and should not be used as a production environment. </p>
-<p>Now that you have been warned, you can download the <a href="/distrib/V8.3-beta0/files/coq-8.3-beta0-1.tar.gz">source files</a>.</p>
+<p>Now that you have been warned, you can download the <a href="https://coq-distrib.s3-website.fr-par.scw.cloud/V8.3-beta0/files/coq-8.3-beta0-1.tar.gz">source files</a>.</p>
 </#def>

news/coq-83-is-out

@@ -15,8 +15,8 @@
 <li>interactive proofs in module types,</li>
 <li>a beautifying coqc option for pretty-printing files</li>
 </ul>
-<p>See the file <a href="/distrib/V8.3/CHANGES">CHANGES</a> for a full log of changes.</p>
-<p>Even if we try to preserve compatibility as much as possible with Coq 8.2, we had to arbitrate for a break of behavior in some situations. The major incompatibilities can be easily treated by using the new <code>-compat 8.2</code> option or by setting/unsetting adequate options. See <a href="/distrib/V8.3/COMPATIBILITY">COMPATIBILITY</a> for details and migration recommendations.</p>
+<p>See the file <a href="https://coq-distrib.s3-website.fr-par.scw.cloud/V8.3/CHANGES">CHANGES</a> for a full log of changes.</p>
+<p>Even if we try to preserve compatibility as much as possible with Coq 8.2, we had to arbitrate for a break of behavior in some situations. The major incompatibilities can be easily treated by using the new <code>-compat 8.2</code> option or by setting/unsetting adequate options. See <a href="https://coq-distrib.s3-website.fr-par.scw.cloud/V8.3/COMPATIBILITY">COMPATIBILITY</a> for details and migration recommendations.</p>
 <p>In addition to the "ssreflect" plugin, extension packages we are aware about include the following (but probably there are more):</p>
 <ul>
 <li>the <code>Heq</code> library for smooth rewriting using heterogeneous equality by C.-K. Hur;</li>

news/coq-83pl2-is-out

@@ -3,5 +3,5 @@
 <#def AUTHOR>herbelin</#def>
 <#def DATE>25 Apr 2011 17:44 GMT</#def>
 <#def DESCR>
-<p>Version 8.3pl2 of Coq fixes several bugs of version 8.3pl1. In particular, it provides compatibility for compiling Coq from sources with the latest versions of Objective Caml and Camlp5. More information to be found in the <a href="/distrib/8.3pl2/CHANGES">CHANGES</a> file.</p>
+<p>Version 8.3pl2 of Coq fixes several bugs of version 8.3pl1. In particular, it provides compatibility for compiling Coq from sources with the latest versions of Objective Caml and Camlp5. More information to be found in the <a href="https://coq-distrib.s3-website.fr-par.scw.cloud/8.3pl2/CHANGES">CHANGES</a> file.</p>
 </#def>

news/coq-83pl3-is-out

@@ -4,5 +4,5 @@
 <#def DATE>27 Dec 2011 10:30 GMT</#def>
 <#def DESCR>
 <p>Version 8.3pl3 of Coq fixes several bugs of version 8.3pl2. At the same time, new patch-level releases of 8.1 and 8.2 have been released to fix critical bugs related to sort-polymorphism of inductive types.</p>
-<p>For 8.3pl3, see the <a href="/distrib/V8.3pl3/CHANGES.updated">CHANGES</a> file for a selected list of changes since 8.3pl2.</p>
+<p>For 8.3pl3, see the <a href="https://coq-distrib.s3-website.fr-par.scw.cloud/V8.3pl3/CHANGES.updated">CHANGES</a> file for a selected list of changes since 8.3pl2.</p>
 </#def>

news/coq-84pl4-is-out

@@ -3,7 +3,7 @@
 <#def AUTHOR>boutillier</#def>
 <#def DATE>12 May 2014 11:11 GMT</#def>
 <#def DESCR>
-<p>Version 8.4pl4 of Coq fixes several bugs of version 8.4pl3 including 3 critical ones. More information to be found in the <a href="/distrib/V8.4pl4/CHANGES">CHANGES</a> file.</p>
+<p>Version 8.4pl4 of Coq fixes several bugs of version 8.4pl3 including 3 critical ones. More information to be found in the <a href="https://coq-distrib.s3-website.fr-par.scw.cloud/V8.4pl4/CHANGES">CHANGES</a> file.</p>
 <p>WARNING: The current logic of Coq is now known to be inconsistent with Axiom prop_extensionality :<br />
 forall A B:Prop, (A &lt;-&gt; B) -&gt; A = B.</p>
 </#def>

news/coq-84pl5-is-out

@@ -3,5 +3,5 @@
 <#def AUTHOR>coq-www</#def>
 <#def DATE>31 Oct 2014 06:11 GMT</#def>
 <#def DESCR>
-<p>Version <a href="/coq-84">8.4pl5</a> of Coq fixes several bugs of version 8.4pl4 including the compatibility with OCaml 4.02. More information to be found in the <a href="/distrib/V8.4pl5/CHANGES">CHANGES</a> file.</p>
+<p>Version <a href="/coq-84">8.4pl5</a> of Coq fixes several bugs of version 8.4pl4 including the compatibility with OCaml 4.02. More information to be found in the <a href="https://coq-distrib.s3-website.fr-par.scw.cloud/V8.4pl5/CHANGES">CHANGES</a> file.</p>
 </#def>

news/coq-84pl6-is-out

@@ -3,5 +3,5 @@
 <#def AUTHOR>coq-www</#def>
 <#def DATE>9 Apr 2015 16:25 GMT</#def>
 <#def DESCR>
-<p>Version <a href="/coq-84">8.4pl6</a> of Coq fixes several bugs of version 8.4pl5. More information to be found in the <a href="/distrib/V8.4pl6/CHANGES">CHANGES</a> file.</p>
+<p>Version <a href="/coq-84">8.4pl6</a> of Coq fixes several bugs of version 8.4pl5. More information to be found in the <a href="https://coq-distrib.s3-website.fr-par.scw.cloud/V8.4pl6/CHANGES">CHANGES</a> file.</p>
 </#def>

news/coq-85-is-out

@@ -22,5 +22,5 @@ brings several major features to Coq:
 </ul>
 
 More information about the changes from 8.4 to 8.5 can be found in the
-<a href="/distrib/V8.5/CHANGES">CHANGES</a> file. Feedback and
+<a href="https://coq-distrib.s3-website.fr-par.scw.cloud/V8.5/CHANGES">CHANGES</a> file. Feedback and
 <a href="/bugs">bug reports</a> are extremely welcome. Enjoy!  </#def>

news/coq-85beta1-is-out

@@ -22,6 +22,6 @@ testing. The 8.5 version brings several major features to Coq:
 </ul>
 
 More information about the changes from 8.4 to 8.5 can be found in
-the <a href="/distrib/V8.5beta1/CHANGES">CHANGES</a> file. Feedback and
+the <a href="https://coq-distrib.s3-website.fr-par.scw.cloud/V8.5beta1/CHANGES">CHANGES</a> file. Feedback and
 <a href="/bugs">bug reports</a> are extremely welcome. Enjoy!
 </#def>

news/coq-85beta2-is-out

@@ -23,5 +23,5 @@ testing. The 8.5 version brings several major features to Coq:
 
 More information about the changes from 8.4 to 8.5 and since the first
 beta release can be found in the <a
-href="/distrib/V8.5beta2/CHANGES">CHANGES</a> file. Feedback and <a
+href="https://coq-distrib.s3-website.fr-par.scw.cloud/V8.5beta2/CHANGES">CHANGES</a> file. Feedback and <a
 href="/bugs">bug reports</a> are extremely welcome. Enjoy!  </#def>

news/coq-85beta3-is-out

@@ -23,5 +23,5 @@ testing. The 8.5 version brings several major features to Coq:
 
 More information about the changes from 8.4 to 8.5 and since the first two
 beta releases can be found in the <a
-href="/distrib/V8.5beta3/CHANGES">CHANGES</a> file. Feedback and <a
+href="https://coq-distrib.s3-website.fr-par.scw.cloud/V8.5beta3/CHANGES">CHANGES</a> file. Feedback and <a
 href="/bugs">bug reports</a> are extremely welcome. Enjoy!  </#def>

news/coq-85pl1-is-out

@@ -6,6 +6,6 @@
 <a href="/coq-85">Version 8.5pl1 of Coq</a> is available. It fixes several bugs
 of version 8.5, including one critical bug. It also brings various performance
 improvements.  More information can be found in the <a
-href="/distrib/V8.5pl1/CHANGES">CHANGES</a> file. Feedback and <a
+href="https://coq-distrib.s3-website.fr-par.scw.cloud/V8.5pl1/CHANGES">CHANGES</a> file. Feedback and <a
 href="/bugs">bug reports</a> are extremely welcome.
 </#def>

news/coq-85pl2-is-out

@@ -5,6 +5,6 @@
 <#def DESCR>
 <a href="/coq-85">Version 8.5pl2 of Coq</a> is available. It fixes several bugs
 of version 8.5pl1, including one critical bug. More information can be found in
-the <a href="/distrib/V8.5pl2/CHANGES">CHANGES</a> file. Feedback and
+the <a href="https://coq-distrib.s3-website.fr-par.scw.cloud/V8.5pl2/CHANGES">CHANGES</a> file. Feedback and
 <a href="/bugs">bug reports</a> are extremely welcome.
 </#def>

news/coq-85pl3-is-out

@@ -5,6 +5,6 @@
 <#def DESCR>
 <a href="/coq-85">Version 8.5pl3 of Coq</a> is available. It fixes several bugs
 of version 8.5pl2, including one critical bug. More information can be found in
-the <a href="/distrib/V8.5pl3/CHANGES">CHANGES</a> file. Feedback and
+the <a href="https://coq-distrib.s3-website.fr-par.scw.cloud/V8.5pl3/CHANGES">CHANGES</a> file. Feedback and
 <a href="/bugs">bug reports</a> are extremely welcome.
 </#def>

news/coq-85rc1-is-out

@@ -23,5 +23,5 @@ testing. The 8.5 version brings several major features to Coq:
 
 More information about the changes from 8.4 to 8.5 and since the
 beta releases can be found in the
-<a href="/distrib/V8.5rc1/CHANGES">CHANGES</a> file. Feedback and
+<a href="https://coq-distrib.s3-website.fr-par.scw.cloud/V8.5rc1/CHANGES">CHANGES</a> file. Feedback and
 <a href="/bugs">bug reports</a> are extremely welcome. Enjoy!  </#def>

news/coq-86-is-out

@@ -32,7 +32,7 @@ Coq 8.6 includes:
 </ul>
 
 <p>More information can be found in the <a
-href="/distrib/V8.6/CHANGES">CHANGES</a> file. Feedback and
+href="https://coq-distrib.s3-website.fr-par.scw.cloud/V8.6/CHANGES">CHANGES</a> file. Feedback and
 <a href="/bugs">bug reports</a> are extremely welcome.</p>
 
 <p>Coq 8.6 initiates a time-based release cycle, with a major version being

news/coq-861-is-out

@@ -5,6 +5,6 @@
 <#def DESCR>
 <a href="/coq-86">Version 8.6.1 of Coq</a> is available. It fixes several bugs
 of version 8.6. More information can be found in the <a
-href="/distrib/V8.6.1/CHANGES">CHANGES</a> file. Feedback and
+href="https://coq-distrib.s3-website.fr-par.scw.cloud/V8.6.1/CHANGES">CHANGES</a> file. Feedback and
 <a href="/bugs">bug reports</a> are extremely welcome.
 </#def>

news/coq-86beta1-is-out

@@ -33,7 +33,7 @@ Coq 8.6 includes:
 </ul>
 
 <p>More information can be found in the <a
-href="/distrib/V8.6beta1/CHANGES">CHANGES</a> file. Feedback and
+href="https://coq-distrib.s3-website.fr-par.scw.cloud/V8.6beta1/CHANGES">CHANGES</a> file. Feedback and
 <a href="/bugs">bug reports</a> are extremely welcome.</p>
 
 <p>Coq 8.6 initiates a time-based release cycle, with a major version being

news/coq-86rc1-is-out

@@ -33,7 +33,7 @@ Coq 8.6 includes:
 </ul>
 
 <p>More information can be found in the <a
-href="/distrib/V8.6rc1/CHANGES">CHANGES</a> file. Feedback and
+href="https://coq-distrib.s3-website.fr-par.scw.cloud/V8.6rc1/CHANGES">CHANGES</a> file. Feedback and
 <a href="/bugs">bug reports</a> are extremely welcome.</p>
 
 <p>Coq 8.6 initiates a time-based release cycle, with a major version being

news/coq-87beta1-is-out

@@ -35,7 +35,7 @@ Coq 8.7 includes:
 </ul>
 
 <p>More information can be found in the <a
-href="/distrib/V8.7+beta1/CHANGES">CHANGES</a> file. Feedback and
+href="https://coq-distrib.s3-website.fr-par.scw.cloud/V8.7+beta1/CHANGES">CHANGES</a> file. Feedback and
 <a href="/bugs">bug reports</a> are extremely welcome.</p>
 
 <p>This is the second release of Coq developed on a time-based development

pages/coq-82-beta-detailed-description.html

@@ -8,7 +8,7 @@
 
 <p>The support for Haskell-style type classes has been contributed by
 M. Sozeau and is documented in <a
-href="/distrib/V8.2/refman//Reference-Manual024.html">chapter
+href="https://coq-distrib.s3-website.fr-par.scw.cloud/V8.2/refman/Reference-Manual024.html">chapter
 18</a> of the reference manual.</p>
 
 <p>The evolutions of the arithmetic libraries cover the following points:</p>
@@ -32,52 +32,52 @@
 </ul>
 
 <p>The <a
-href="/distrib/V8.2/refman//Reference-Manual007.html">module
+href="https://coq-distrib.s3-website.fr-par.scw.cloud/V8.2/refman/Reference-Manual007.html">module
 system</a> has been extended with the include feature, sharing of
 common submodules, functorial signature application and on-demand
 parameter inlining (E. Soubiran).</p>
 
 
 <p>At the level of tactics, Coq 8.2 offers a more efficient
 implementation of <a
-href="/distrib/V8.2/refman//Reference-Manual029.html">setoid
+href="https://coq-distrib.s3-website.fr-par.scw.cloud/V8.2/refman/Reference-Manual029.html">setoid
 rewrite</a>, new support for constant unfolding in apply, new <a
-href="/distrib/V8.2/refman//Reference-Manual011.html#@tactic84">dependent
+href="https://coq-distrib.s3-website.fr-par.scw.cloud/V8.2/refman/Reference-Manual011.html#@tactic84">dependent
 induction</a>, <a
-href="/distrib/V8.2/refman//Reference-Manual011.html#@tactic69">induction</a>/<a
-href="/distrib/V8.2/refman//Reference-Manual011.html#@tactic75">destruct</a>
+href="https://coq-distrib.s3-website.fr-par.scw.cloud/V8.2/refman/Reference-Manual011.html#@tactic69">induction</a>/<a
+href="https://coq-distrib.s3-website.fr-par.scw.cloud/V8.2/refman/Reference-Manual011.html#@tactic75">destruct</a>
 with "in" clause and "e" variants, support for <a
-href="/distrib/V8.2/refman//Reference-Manual011.html#@tactic94">iteration
+href="https://coq-distrib.s3-website.fr-par.scw.cloud/V8.2/refman/Reference-Manual011.html#@tactic94">iteration
 and "at" clause in rewrite</a>, new variants of <a
-href="/distrib/V8.2/refman//Reference-Manual011.html#@tactic82">introduction
+href="https://coq-distrib.s3-website.fr-par.scw.cloud/V8.2/refman/Reference-Manual011.html#@tactic82">introduction
 patterns</a>, support for implicit contents and coercions in the
 "with" clauses, use of type informations in unification (P. Letouzey,
 M. Sozeau, S. Glondu, E. Makarov, H. Herbelin). The mathematical proof
 language is documented in <a
-href="/distrib/V8.2/refman//Reference-Manual014.html">chapter
+href="https://coq-distrib.s3-website.fr-par.scw.cloud/V8.2/refman/Reference-Manual014.html">chapter
 11</a> of the reference manual (P. Corbineau).</p>
 
 <p>Coq 8.2 also offers miscellaneous syntax extensions and improved
-features: <a href="/distrib/V8.2/refman//Reference-Manual004.html#@default69">destructing let</a>, better type inference,
+features: <a href="https://coq-distrib.s3-website.fr-par.scw.cloud/V8.2/refman/Reference-Manual004.html#@default69">destructing let</a>, better type inference,
 inference of matching return clause, detection of impossible clause in
 dependent pattern-matching, detection of decreasing argument in
-fixpoints, improved <a href="/distrib/V8.2/refman//Reference-Manual027.html">Program</a> and <a href="/distrib/V8.2/refman//Reference-Manual004.html#toc15">Function</a>
-features, new ways to work with <a href="/distrib/V8.2/refman//Reference-Manual004.html#toc19">implicit arguments</a>, and
+fixpoints, improved <a href="https://coq-distrib.s3-website.fr-par.scw.cloud/V8.2/refman/Reference-Manual027.html">Program</a> and <a href="https://coq-distrib.s3-website.fr-par.scw.cloud/V8.2/refman/Reference-Manual004.html#toc15">Function</a>
+features, new ways to work with <a href="https://coq-distrib.s3-website.fr-par.scw.cloud/V8.2/refman/Reference-Manual004.html#toc19">implicit arguments</a>, and
 various other auxiliary features (M. Sozeau, P. Letouzey,
 H. Herbelin). It also provides automatic generation of decidable
 equality (V. Siles).</p>
 
 <p>Finally, Coq comes with a new stand-alone <a
-href="/distrib/V8.2/refman//Reference-Manual017.html#toc89">checker</a>
+href="https://coq-distrib.s3-website.fr-par.scw.cloud/V8.2/refman/Reference-Manual017.html#toc89">checker</a>
 for cross-certification of vo-files (B. Barras).</p>
 
-<p>For all other changes, see the <a href="/distrib/V8.2/CHANGES">CHANGES</a> file.</p>
+<p>For all other changes, see the <a href="https://coq-distrib.s3-website.fr-par.scw.cloud/V8.2/CHANGES">CHANGES</a> file.</p>
 
 <p>As far as we could judge, the major sources of incompatibilities come
 from the new implementation of setoid rewrite and, marginally, from
 the support of constant unfolding in apply. A secondary source comes
 from some bug fixes and from changes in specific libraries. See the <a
-href="/distrib/V8.2/COMPATIBILITY">COMPATIBILITY</a> file for details and smooth
+href="https://coq-distrib.s3-website.fr-par.scw.cloud/V8.2/COMPATIBILITY">COMPATIBILITY</a> file for details and smooth
 migration recommendations. We are interested in feedback on the
 upgrading problems that may be encountered.</p>