From bc480550dbd705384bec15968dbdde0987df311c Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Tue, 31 Mar 2015 09:25:29 +0200
Subject: Do not escape "'" when outputting to html, especially not using
 "´".

---
 tools/coqdoc/output.ml | 1 -
 1 file changed, 1 deletion(-)

(limited to 'tools')

diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml
index ae6e6388f0..06030c45a6 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


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(-)

(limited to 'tools')

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