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 --- doc/index.html | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'doc') 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.