diff options
| author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2013-01-11 13:08:04 +0000 |
|---|---|---|
| committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2013-01-11 13:08:04 +0000 |
| commit | 34d58b781afec8ecd4afdcf2ab83f1c972338ba9 (patch) | |
| tree | 1f4e873a35261b4d1e15004d25ef688ce6b74ce5 /doc/coq2html.mll | |
| parent | 93a33f710ed9a5eb045d8ee09b6142142b172f18 (diff) | |
| download | compcert-34d58b781afec8ecd4afdcf2ab83f1c972338ba9.tar.gz compcert-34d58b781afec8ecd4afdcf2ab83f1c972338ba9.zip | |
Updated documentationv1.12
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2098 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'doc/coq2html.mll')
| -rw-r--r-- | doc/coq2html.mll | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/doc/coq2html.mll b/doc/coq2html.mll index b10815c1..9c30bea6 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." | ("Proof" space+ "with") | ("Next" space+ "Obligation.") +let start_proof = ("Proof" space* ".") | ("Proof" space+ "with") | ("Next" space+ "Obligation.") let end_proof = "Qed." | "Defined." | "Save." | "Admitted." | "Abort." let xref = ['A'-'Z' 'a'-'z' '0'-'9' '_' '.']+ | "<>" @@ -370,7 +370,7 @@ and globfile = parse | "F" (ident as m) space* "\n" { current_module := m; add_module m; globfile lexbuf } - | "R" (integer as pos) + | "R" (integer as pos) ":" (integer as pos2) space+ (xref as dp) space+ (xref as sp) space+ (xref as id) @@ -379,7 +379,7 @@ and globfile = parse { add_reference !current_module (int_of_string pos) dp sp id ty; globfile lexbuf } | (ident as ty) - space+ (integer as pos) + space+ (integer as pos) ":" (integer as pos2) space+ (xref as sp) space+ (xref as id) space* "\n" |