diff options
| -rw-r--r-- | common/Values.v | 2 | ||||
| -rw-r--r-- | doc/coq2html.mll | 6 | ||||
| -rw-r--r-- | doc/index.html | 22 |
3 files changed, 15 insertions, 15 deletions
diff --git a/common/Values.v b/common/Values.v index 9f73e33..1c03789 100644 --- a/common/Values.v +++ b/common/Values.v @@ -1107,7 +1107,7 @@ Proof. unfold inject_incr. auto. Qed. Lemma inject_incr_trans : forall f1 f2 f3, inject_incr f1 f2 -> inject_incr f2 f3 -> inject_incr f1 f3 . -Proof . +Proof. unfold inject_incr; intros. eauto. Qed. diff --git a/doc/coq2html.mll b/doc/coq2html.mll index b10815c..9c30bea 100644 --- a/doc/coq2html.mll +++ b/doc/coq2html.mll @@ -249,7 +249,7 @@ let end_html_page () = let space = [' ' '\t'] let ident = ['A'-'Z' 'a'-'z' '_'] ['A'-'Z' 'a'-'z' '0'-'9' '_']* let path = ident ("." ident)* -let start_proof = "Proof." | ("Proof" space+ "with") | ("Next" space+ "Obligation.") +let start_proof = ("Proof" space* ".") | ("Proof" space+ "with") | ("Next" space+ "Obligation.") let end_proof = "Qed." | "Defined." | "Save." | "Admitted." | "Abort." let xref = ['A'-'Z' 'a'-'z' '0'-'9' '_' '.']+ | "<>" @@ -370,7 +370,7 @@ and globfile = parse | "F" (ident as m) space* "\n" { current_module := m; add_module m; globfile lexbuf } - | "R" (integer as pos) + | "R" (integer as pos) ":" (integer as pos2) space+ (xref as dp) space+ (xref as sp) space+ (xref as id) @@ -379,7 +379,7 @@ and globfile = parse { add_reference !current_module (int_of_string pos) dp sp id ty; globfile lexbuf } | (ident as ty) - space+ (integer as pos) + space+ (integer as pos) ":" (integer as pos2) space+ (xref as sp) space+ (xref as id) space* "\n" diff --git a/doc/index.html b/doc/index.html index 172e18e..aa1847f 100644 --- a/doc/index.html +++ b/doc/index.html @@ -1,7 +1,7 @@ <!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN"> <HTML> <HEAD> -<TITLE>The Compcert verified compiler</TITLE> +<TITLE>The CompCert verified compiler</TITLE> <META HTTP-EQUIV="Content-Type" CONTENT="text/html; charset=iso-8859-1"> <style type="text/css"> @@ -22,21 +22,21 @@ a:active {color : Red; text-decoration : underline; } </HEAD> <BODY> -<H1 align="center">The Compcert verified compiler</H1> +<H1 align="center">The CompCert verified compiler</H1> <H2 align="center">Commented Coq development</H2> <H3 align="center">Version 1.12, 2013-01-11</H3> <H2>Introduction</H2> -<P>Compcert is a compiler that generates PowerPC, ARM and x86 assembly -code from Compcert C, a large subset of the C programming language. +<P>CompCert is a compiler that generates PowerPC, ARM and x86 assembly +code from CompCert C, a large subset of the C programming language. The particularity of this compiler is that it is written mostly within the specification language of the Coq proof assistant, and its correctness --- the fact that the generated assembly code is semantically equivalent to its source program --- was entirely proved within the Coq proof assistant.</P> -<P>High-level descriptions of the Compcert compiler and its proof of +<P>High-level descriptions of the CompCert compiler and its proof of correctness can be found in the following papers (in increasing order of technical details):</P> <UL> <LI>Xavier Leroy, <A HREF="http://gallium.inria.fr/~xleroy/publi/compcert-CACM.pdf">Formal verification of a realistic compiler</A>. Communications of the ACM 52(7), July 2009. @@ -59,10 +59,10 @@ versions can be found in the source distribution. substantially changed since the overview papers above were written.</P> -<P>The complete sources for Compcert can be downloaded from -<A HREF="http://compcert.inria.fr/">the Compcert Web site</A>.</P> +<P>The complete sources for CompCert can be downloaded from +<A HREF="http://compcert.inria.fr/">the CompCert Web site</A>.</P> -<P>This document and the Compcert sources are +<P>This document and the CompCert sources are copyright 2005, 2006, 2007, 2008, 2009, 2010, 2011, 2012, 2013 Institut National de Recherche en Informatique et en Automatique (INRIA) and distributed under the terms of the @@ -112,7 +112,7 @@ semantics. <H3>Source, intermediate and target languages: syntax and semantics</H3> <UL> -<LI> The Compcert C source language: +<LI> The CompCert C source language: <A HREF="html/Csyntax.html">syntax</A> and <A HREF="html/Csem.html">semantics</A> and <A HREF="html/Cstrategy.html">determinized semantics</A>.<BR> @@ -159,7 +159,7 @@ code. <TR valign="top"> <TD>Pulling side-effects out of expressions;<br> fixing an evaluation order</TD> - <TD>Compcert C to Clight</TD> + <TD>CompCert C to Clight</TD> <TD><A HREF="html/SimplExpr.html">SimplExpr</A></TD> <TD><A HREF="html/SimplExprspec.html">SimplExprspec</A><br> <A HREF="html/SimplExprproof.html">SimplExprproof</A></TD> @@ -168,7 +168,7 @@ code. <TD>Pulling non-adressable scalar local variables out of memory</TD> <TD>Clight to Clight</TD> <TD><A HREF="html/SimplLocals.html">SimplLocals</A></TD> - <A HREF="html/SimplLocalsproof.html">SimplLocalsproof</A></TD> + <TD><A HREF="html/SimplLocalsproof.html">SimplLocalsproof</A></TD> </TR> <TR valign="top"> <TD>Simplification of control structures; <br> |