summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--doc/coq2html.mll2
-rw-r--r--doc/index.html3
2 files changed, 3 insertions, 2 deletions
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.