From 34d58b781afec8ecd4afdcf2ab83f1c972338ba9 Mon Sep 17 00:00:00 2001 From: xleroy Date: Fri, 11 Jan 2013 13:08:04 +0000 Subject: Updated documentation git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2098 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- doc/coq2html.mll | 6 +++--- doc/index.html | 22 +++++++++++----------- 2 files changed, 14 insertions(+), 14 deletions(-) (limited to 'doc') diff --git a/doc/coq2html.mll b/doc/coq2html.mll index b10815c..9c30bea 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" diff --git a/doc/index.html b/doc/index.html index 172e18e..aa1847f 100644 --- a/doc/index.html +++ b/doc/index.html @@ -1,7 +1,7 @@ -The Compcert verified compiler +The CompCert verified compiler