Update Coq documentation

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2483 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

2 files changed, 4 insertions, 4 deletions

diff --git a/Makefile b/Makefile
index 9ab503b..9cad0e8 100644
--- a/Makefile
+++ b/Makefile
@@ -194,7 +194,7 @@ documentation: doc/coq2html $(FILES)
 	mkdir -p doc/html
 	rm -f doc/html/*.html
 	doc/coq2html -o 'doc/html/%.html' doc/*.glob \
-          $(filter-out doc/coq2html, $^)
+          $(filter-out doc/coq2html cparser/Parser.v, $^)
 	cp doc/coq2html.css doc/coq2html.js doc/html/
 
 doc/coq2html: doc/coq2html.ml
diff --git a/doc/index.html b/doc/index.html
index 1845851..296d89e 100644
--- a/doc/index.html
+++ b/doc/index.html
@@ -24,7 +24,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 2.2, 2014-02-24</H3>
+<H3 align="center">Version 2.3, 2015-05-05</H3>
 
 <H2>Introduction</H2>
 
@@ -106,7 +106,7 @@ See also: <A HREF="html/Memdata.html">Memdata</A> (in-memory representation of d
 <LI> <A HREF="html/Determinism.html">Determinism</A>: determinism properties of small-step semantics.
 <LI> <A HREF="html/Op.html"><I>Op</I></A>: operators, addressing modes and their
 semantics.
-<LI> <A HREF="html/Subtyping.html">Subtyping</A>: a solver for atomic subtyping constraints.
+<LI> <A HREF="html/Unityping.html">Unityping</A>: a solver for atomic unification constraints.
 </UL>
 
 <H3>Source, intermediate and target languages: syntax and semantics</H3>
@@ -315,7 +315,7 @@ See also: <A HREF="html/NeedOp.html"><I>NeedOp</I></A>: processor-dependent part
 
 <H3>Type systems</H3>
 
-Trivial type systems are used to statically capture well-formedness
+Simple type systems are used to statically capture well-formedness
 conditions on some intermediate languages.
 <UL>
 <LI> <A HREF="html/RTLtyping.html">RTLtyping</A>: typing for RTL + type