From 0aa2544d04dbd4b6ee665b551ed165e4fb02d2fa Mon Sep 17 00:00:00 2001
From: Enrico Tassi <gareuselesinge@debian.org>
Date: Wed, 15 Jul 2015 10:36:12 +0200
Subject: Imported Upstream version 8.5~beta2+dfsg

---
 tools/coqdoc/cpretty.mll | 12 +++---------
 tools/coqdoc/output.ml   |  1 -
 2 files changed, 3 insertions(+), 10 deletions(-)

(limited to 'tools/coqdoc')

diff --git a/tools/coqdoc/cpretty.mll b/tools/coqdoc/cpretty.mll
index edf7ee8e..cb704146 100644
--- a/tools/coqdoc/cpretty.mll
+++ b/tools/coqdoc/cpretty.mll
@@ -405,7 +405,7 @@ let set_kw =
 
 let gallina_kw_to_hide =
     "Implicit" space+ "Arguments"
-  | "Ltac"
+  | ("Local" space+)? "Ltac"
   | "Require"
   | "Import"
   | "Export"
@@ -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
diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml
index ae6e6388..06030c45 100644
--- a/tools/coqdoc/output.ml
+++ b/tools/coqdoc/output.ml
@@ -595,7 +595,6 @@ module Html = struct
 	| '<' -> Buffer.add_string buff "&lt;"
 	| '>' -> Buffer.add_string buff "&gt;"
 	| '&' -> Buffer.add_string buff "&amp;"
-        | '\'' -> Buffer.add_string buff "&acute;"
         | '\"' -> Buffer.add_string buff "&quot;"
 	| c -> Buffer.add_char buff c
       done;
-- 
cgit v1.2.3