aboutsummaryrefslogtreecommitdiff
path: root/tools
diff options
context:
space:
mode:
Diffstat (limited to 'tools')
-rw-r--r--tools/coqdoc/cpretty.mll4
1 files changed, 3 insertions, 1 deletions
diff --git a/tools/coqdoc/cpretty.mll b/tools/coqdoc/cpretty.mll
index 27e8f0b963..d11b12477d 100644
--- a/tools/coqdoc/cpretty.mll
+++ b/tools/coqdoc/cpretty.mll
@@ -269,7 +269,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' ] | *)