aboutsummaryrefslogtreecommitdiffhomepage
path: root/tools/coqdoc/cpretty.mll
diff options
context:
space:
mode:
authorGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2010-12-06 23:55:04 +0000
committerGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2010-12-06 23:55:04 +0000
commitd5d17c7813526188ad4f94eb85a27ce9f20a4e5c (patch)
tree6d5bbce5c8524a44e4a61ebcd055deb87ff71f4b /tools/coqdoc/cpretty.mll
parent9764ebbb67edf73a147c536a3c4f4ed0f1a7ce9e (diff)
Fixed status of ÷ and × in coqdoc (they were seen as letter instead of symbol).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13691 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tools/coqdoc/cpretty.mll')
-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 27e8f0b96..d11b12477 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' ] | *)