diff options
| author |  xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2011-08-23 11:45:14 +0000 |
|---|---|---|
| committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2011-08-23 11:45:14 +0000 |
| commit | ca0117ca268873766ac4fda3771295842b17fcd6 (patch) | |
| tree | a4558d7703fede5c4045748a2e9fed11173cdcac /doc/coq2html.mll | |
| parent | 8c697ac826f8bcac956fe8a6c6356a6c459d3c92 (diff) | |
Doc fixes
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1726 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'doc/coq2html.mll')
| -rw-r--r-- | doc/coq2html.mll | 2 |
1 files changed, 1 insertions, 1 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' '_' '.']+ | "<>" |