diff options
| -rw-r--r-- | doc/coq2html.mll | 2 | ||||
| -rw-r--r-- | doc/index.html | 3 |
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. |