From 6019b688884901ee2a51fb0d1b4318b259c99bfc Mon Sep 17 00:00:00 2001 From: xleroy Date: Mon, 5 May 2014 14:01:22 +0000 Subject: Update Coq documentation git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2483 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- Makefile | 2 +- doc/index.html | 6 +++--- 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; }

The CompCert verified compiler

Commented Coq development

-

Version 2.2, 2014-02-24

+

Version 2.3, 2015-05-05

Introduction

@@ -106,7 +106,7 @@ See also: Memdata (in-memory representation of d
  • Determinism: determinism properties of small-step semantics.
  • Op: operators, addressing modes and their semantics. -
  • Subtyping: a solver for atomic subtyping constraints. +
  • Unityping: a solver for atomic unification constraints.

    Source, intermediate and target languages: syntax and semantics

    @@ -315,7 +315,7 @@ See also: NeedOp: processor-dependent part

    Type systems

    -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.