From 6b05ae1c447680cd4ed1332c0c8b4f0e24b33f03 Mon Sep 17 00:00:00 2001
From: Karl Palmskog
Date: Mon, 13 Jan 2020 14:59:22 -0600
Subject: [coqdoc] Fix #11353: coqdoc -g omits all sentences with decorations

---
 tools/coqdoc/cpretty.mll | 8 ++++++++
 1 file changed, 8 insertions(+)

(limited to 'tools')

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
       { () }
-- 
cgit v1.2.3