From 89234ade11c126ec6ff625c56096cac2cc58c120 Mon Sep 17 00:00:00 2001 From: xleroy Date: Wed, 17 Oct 2007 08:56:17 +0000 Subject: MAJ git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@421 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- doc/index.html | 9 ++++----- doc/removeproofs | 2 ++ 2 files changed, 6 insertions(+), 5 deletions(-) (limited to 'doc') 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 @@ -The Compcert certified compiler +The Compcert verified compiler - -

The Compcert certified compiler

The Compcert verified compiler

Commented Coq development

Version 1.0, 2007-08-28

Version 1.1, 2007-09-17

Introduction

@@ -236,7 +235,7 @@ code. Mach to Mach (none) PPCgenretaddr
- Machabstr2mach + Machabstr2concr Emission of PowerPC assembly 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 '/Proof<\/span> *\./,/$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 -- cgit v1.2.3