From ca0117ca268873766ac4fda3771295842b17fcd6 Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Tue, 23 Aug 2011 11:45:14 +0000
Subject: Doc fixes

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1726 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
---
 doc/coq2html.mll | 2 +-
 doc/index.html   | 3 ++-
 2 files changed, 3 insertions(+), 2 deletions(-)

(limited to 'doc')

diff --git a/doc/coq2html.mll b/doc/coq2html.mll
index 566e066..b10815c 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." | ("Next" space+ "Obligation.")
+let start_proof = "Proof." | ("Proof" space+ "with") | ("Next" space+ "Obligation.")
 let end_proof = "Qed." | "Defined." | "Save." | "Admitted." | "Abort."
 
 let xref = ['A'-'Z' 'a'-'z' '0'-'9' '_' '.']+ | "<>"
diff --git a/doc/index.html b/doc/index.html
index 84d2905..1fd7859 100644
--- a/doc/index.html
+++ b/doc/index.html
@@ -112,7 +112,8 @@ semantics.
 <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>.
+<A HREF="html/Cstrategy.html">determinized semantics</A>.<BR>
+See also: <A HREF="html/Cexec.html">reference interpreter</A>.
 <LI> <A HREF="html/Clight.html">Clight</A>: a simpler version of Cmedium where expressions contain no side-effects.
 <LI> <A HREF="html/Csharpminor.html">Csharpminor</A>: low-level
  structured language.
-- 
cgit v1.2.3