aboutsummaryrefslogtreecommitdiffstats
path: root/doc
diff options
context:
space:
mode:
authorXavier Leroy <xavier.leroy@college-de-france.fr>2021-05-09 18:08:26 +0200
committerXavier Leroy <xavier.leroy@college-de-france.fr>2021-05-09 18:08:26 +0200
commitb42705f033ff0b70247e13c9589084fd9698ae90 (patch)
tree0d13b9990452fa54901b4e5764e3e4e233a64813 /doc
parent19e1039a26b01297e19590340d7acb25a49b0560 (diff)
downloadcompcert-kvx-b42705f033ff0b70247e13c9589084fd9698ae90.tar.gz
compcert-kvx-b42705f033ff0b70247e13c9589084fd9698ae90.zip
Update for release 3.9
Also: limit the max width of the page, to avoid very long lines.
Diffstat (limited to 'doc')
-rw-r--r--doc/index.html9
1 files changed, 5 insertions, 4 deletions
diff --git a/doc/index.html b/doc/index.html
index ec8c4d91..c3912cb2 100644
--- a/doc/index.html
+++ b/doc/index.html
@@ -8,6 +8,7 @@
body {
color: black; background: white;
margin-left: 5%; margin-right: 5%;
+ max-width:750px;
}
h2 { margin-left: -5%;}
h3 { margin-left: -3%; }
@@ -24,7 +25,7 @@ a:active {color : Red; text-decoration : underline; }
<H1 align="center">The CompCert verified compiler</H1>
<H2 align="center">Commented Coq development</H2>
-<H3 align="center">Version 3.8, 2020-11-16</H3>
+<H3 align="center">Version 3.9, 2021-05-10</H3>
<H2>Introduction</H2>
@@ -46,9 +47,9 @@ Journal of Automated Reasoning 43(4):363-446, 2009.
<P>This Web site gives a commented listing of the underlying Coq
specifications and proofs. Proof scripts are folded by default, but
-can be viewed by clicking on "Proof". Some modules (written in <I>italics</I> below) differ between the four target architectures. The
-PowerPC versions of these modules are shown below; the ARM, x86 and RISC-V
-versions can be found in the source distribution.
+can be viewed by clicking on "Proof". Some modules (written in <I>italics</I> below) differ between the five target architectures. The
+PowerPC versions of these modules are shown below; the AArch64, ARM,
+x86 and RISC-V versions can be found in the source distribution.
</P>
<P> This development is a work in progress; some parts have