From 68881dcdf8be4c4ee8368574cf20cd2a38d383f9 Mon Sep 17 00:00:00 2001
From: xleroy
Date: Wed, 19 Mar 2008 09:53:21 +0000
Subject: Revu removeproof
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@567 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
---
doc/index.html | 22 +++++++++-------------
1 file changed, 9 insertions(+), 13 deletions(-)
(limited to 'doc/index.html')
diff --git a/doc/index.html b/doc/index.html
index 1366a849..219e587e 100644
--- a/doc/index.html
+++ b/doc/index.html
@@ -24,7 +24,7 @@ a:active {color : Red; text-decoration : underline; }
The Compcert verified compiler
Commented Coq development
-Version 1.1, 2007-09-17
+Version 1.2, 2008-02-13
Introduction
@@ -55,11 +55,14 @@ compiler written directly in Caml are omitted. This development is a
work in progress; some parts have substantially changed since the
overview papers above were written.
-This document and all Coq source files referenced from it are
-copyright 2005, 2006, 2007 Institut National de Recherche en Informatique et
-en Automatique (INRIA) and distributed under the terms of the GNU General Public
-License version 2.
+The complete sources for Compcert can be downloaded from
+the Compcert Web site.
+
+This document and the Compcert sources are
+copyright 2005, 2006, 2007, 2008 Institut National de Recherche en
+Informatique et en Automatique (INRIA) and distributed under the terms
+of the following license.
+
Table of contents
@@ -67,14 +70,8 @@ License version 2.
- Coqlib: addendum to the Coq standard library.
- (Coq source file with proofs:
-
Coqlib.v
.)
- Maps: finite maps.
- (Coq source file with proofs:
-
Maps.v
.)
- Integers: machine integers.
- (Coq source file with proofs:
-
Integers.v
.)
- Floats: machine floating-point numbers.
- Iteration: various forms of "while" loops.
- Ordered: construction of
@@ -92,7 +89,6 @@ inequations by fixpoint iteration.
- Errors: the Error monad.
- AST: identifiers, whole programs and other
common elements of abstract syntaxes.
- (Coq source file with proofs:
AST.v
.)
- Values: run-time values.
- Events: observable events and traces.
- Mem: the memory model.
--
cgit