aboutsummaryrefslogtreecommitdiff
path: root/tools
diff options
context:
space:
mode:
authorHugo Herbelin2020-01-14 22:04:27 +0100
committerHugo Herbelin2020-01-14 22:04:27 +0100
commit7c51a2571112d5f913fbbc22bdd79cbca92db1cd (patch)
tree01b54eac55142eee0cd364513cfa5f803abf554b /tools
parent8b4f78ded7269139c7e9c222c6382a788c48039a (diff)
parent6b05ae1c447680cd4ed1332c0c8b4f0e24b33f03 (diff)
Merge PR #11394: [coqdoc] Fix #11353: coqdoc -g omits all sentences with decorations
Ack-by: Zimmi48 Reviewed-by: herbelin
Diffstat (limited to 'tools')
-rw-r--r--tools/coqdoc/cpretty.mll8
1 files changed, 8 insertions, 0 deletions
diff --git a/tools/coqdoc/cpretty.mll b/tools/coqdoc/cpretty.mll
index a44ddf7467..13913cabc3 100644
--- a/tools/coqdoc/cpretty.mll
+++ b/tools/coqdoc/cpretty.mll
@@ -547,6 +547,9 @@ rule coq_bol = parse
comment lexbuf
end else skipped_comment lexbuf in
if eol then coq_bol lexbuf else coq lexbuf }
+ | space* "#[" {
+ let eol = begin backtrack lexbuf; body_bol lexbuf end
+ in if eol then coq_bol lexbuf else coq lexbuf }
| eof
{ () }
| _
@@ -643,6 +646,11 @@ and coq = parse
Output.ident s None;
let eol = body lexbuf in
if eol then coq_bol lexbuf else coq lexbuf }
+ | "#["
+ { ignore(lexeme lexbuf);
+ Output.char '#'; Output.char '[';
+ let eol = body lexbuf in
+ if eol then coq_bol lexbuf else coq lexbuf }
| space+ { Output.char ' '; coq lexbuf }
| eof
{ () }