diff options
| author |  xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2007-10-17 08:56:17 +0000 |
|---|---|---|
| committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2007-10-17 08:56:17 +0000 |
| commit | 89234ade11c126ec6ff625c56096cac2cc58c120 (patch) | |
| tree | ee8cfe576a2e9f9e8d73c51778c5b6f9de996ea8 /doc | |
| parent | 0d2f4a416abcc44fb000758a134a38562a5d6d19 (diff) | |
MAJ
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@421 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/index.html | 9 | ||||
| -rwxr-xr-x | doc/removeproofs | 2 |
2 files changed, 6 insertions, 5 deletions
diff --git a/doc/index.html b/doc/index.html index 4390c87..1366a84 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 certified compiler</TITLE> +<TITLE>The Compcert verified compiler</TITLE> <META HTTP-EQUIV="Content-Type" CONTENT="text/html; charset=iso-8859-1"> <style type="text/css"> @@ -19,13 +19,12 @@ a:hover {color : Red; text-decoration : underline; } a:active {color : Red; text-decoration : underline; } </style> -<LINK type="text/css" rel="stylesheet" href="style.css"> </HEAD> <BODY> -<H1 align="center">The Compcert certified compiler</H1> +<H1 align="center">The Compcert verified compiler</H1> <H2 align="center">Commented Coq development</H2> -<H3 align="center">Version 1.0, 2007-08-28</H3> +<H3 align="center">Version 1.1, 2007-09-17</H3> <H2>Introduction</H2> @@ -236,7 +235,7 @@ code. <TD>Mach to Mach</TD> <TD>(none) <TD><A HREF="html/PPCgenretaddr.html">PPCgenretaddr</A><BR> - <A HREF="html/Machabstr2mach.html">Machabstr2mach</A></TD> + <A HREF="html/Machabstr2concr.html">Machabstr2concr</A></TD> <TR valign="top"> <TD>Emission of PowerPC assembly</TD> diff --git a/doc/removeproofs b/doc/removeproofs index 5ae9a23..266711f 100755 --- a/doc/removeproofs +++ b/doc/removeproofs @@ -4,6 +4,8 @@ for i in $*; do mv $i $i.bak sed -e '/<span class="keyword">Proof<\/span> *\./,/<span class="keyword">\(Qed\|Defined\)<\/span> *\./d' \ -e "s/\"'do' X <- A ; B\" error_monad_scope/doXAB error_monad_scope/g" \ + -e "s/\"'do' X <- A ; B\"/doXAB/g" \ + -e "s/\"'do' ( X , Y ) <- A ; B\"/doXYAB/g" \ $i.bak > $i rm $i.bak done |