From 6b691bbd2101fd39395c0d2135fd7c06a8915e14 Mon Sep 17 00:00:00 2001
From: Stephane Glondu <steph@glondu.net>
Date: Fri, 24 Dec 2010 11:53:29 +0100
Subject: Imported Upstream version 8.3pl1

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

(limited to 'tools/coqdoc/cpretty.mll')

diff --git a/tools/coqdoc/cpretty.mll b/tools/coqdoc/cpretty.mll
index a23a4f74..177058b3 100644
--- a/tools/coqdoc/cpretty.mll
+++ b/tools/coqdoc/cpretty.mll
@@ -7,7 +7,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: cpretty.mll 13440 2010-09-19 20:21:12Z herbelin $ i*)
+(*i $Id: cpretty.mll 13692 2010-12-06 23:55:10Z herbelin $ i*)
 
 (*s Utility functions for the scanners *)
 
@@ -272,7 +272,9 @@ let firstchar =
   (* superscript 1 *)
   '\194' '\185' |
   (* utf-8 latin 1 supplement *)
-  '\195' ['\128'-'\191'] |
+  '\195' ['\128'-'\150'] |
+  '\195' ['\152'-'\182'] |
+  '\195' ['\184'-'\191'] |
   (* utf-8 letterlike symbols *)
   (* '\206' ([ '\145' - '\183'] | '\187') | *)
   (* '\xCF' [ '\x00' - '\xCE' ] |  *)
@@ -315,7 +317,6 @@ let def_token =
   | "Class"
   | "SubClass"
   | "Example"
-  | "Local"
   | "Fixpoint"
   | "Boxed"
   | "CoFixpoint"
@@ -450,6 +451,12 @@ 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
       { let s = lexeme lexbuf in
 	  if !Cdglobals.light && section_or_end s then
-- 
cgit v1.2.3