summaryrefslogtreecommitdiff
path: root/doc/coq2html.mll
diff options
context:
space:
mode:
Diffstat (limited to 'doc/coq2html.mll')
-rw-r--r--doc/coq2html.mll2
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' '_' '.']+ | "<>"