From 4226e7ac76ee8a292b717a3c0c12ef0c60495e90 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Thu, 2 Apr 2015 19:26:27 +0200
Subject: Avoid outputting stray "Local" keywords in HTML documentation.

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

diff --git a/tools/coqdoc/cpretty.mll b/tools/coqdoc/cpretty.mll
index 20dd69f826..cb70414675 100644
--- a/tools/coqdoc/cpretty.mll
+++ b/tools/coqdoc/cpretty.mll
@@ -456,13 +456,7 @@ rule coq_bol = parse
       { begin_show (); coq_bol lexbuf }
   | space* end_show
       { end_show (); coq_bol lexbuf }
-  | space* ("Local"|"Global")
-      {
-	in_proof := None;
-	let s = lexeme lexbuf in
-	output_indented_keyword s lexbuf;
-	coq_bol lexbuf }
-  | space* gallina_kw_to_hide
+  | space* (("Local"|"Global") space+)? gallina_kw_to_hide
       { let s = lexeme lexbuf in
 	  if !Cdglobals.light && section_or_end s then
 	    let eol = skip_to_dot lexbuf in
@@ -596,7 +590,7 @@ and coq = parse
 	end }
   | eof
       { () }
-  | gallina_kw_to_hide
+  | (("Local"|"Global") space+)? gallina_kw_to_hide
       { let s = lexeme lexbuf in
 	  if !Cdglobals.light && section_or_end s then
 	    begin
-- 
cgit v1.2.3