diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-10-21 21:35:49 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-10-22 11:04:30 +0200 |
| commit | 04a7118e26ed3bb3b98ed68a394f7eaed2a0cb81 (patch) | |
| tree | c3190d60c3d935766f357d589204b2c8d728b034 /tools/coqdoc | |
| parent | 2f08f9de37c8e4cee4787e98136886f090e0eafb (diff) | |
Supporting Greek and Coptic (U0370) as first letter of coqdoc identifiers.
Diffstat (limited to 'tools/coqdoc')
| -rw-r--r-- | tools/coqdoc/cpretty.mll | 6 |
1 files changed, 2 insertions, 4 deletions
diff --git a/tools/coqdoc/cpretty.mll b/tools/coqdoc/cpretty.mll index d6eb68882..ea274a8c4 100644 --- a/tools/coqdoc/cpretty.mll +++ b/tools/coqdoc/cpretty.mll @@ -262,10 +262,8 @@ let firstchar = '\195' ['\152'-'\182'] | '\195' ['\184'-'\191'] | (* utf-8 letterlike symbols *) - (* '\206' ([ '\145' - '\183'] | '\187') | *) - (* '\xCF' [ '\x00' - '\xCE' ] | *) - (* utf-8 letterlike symbols *) - '\206' (['\145'-'\161'] | ['\163'-'\187']) | + '\206' (['\145'-'\161'] | ['\163'-'\191']) | + '\207' (['\145'-'\191']) | '\226' ('\130' [ '\128'-'\137' ] (* subscripts *) | '\129' [ '\176'-'\187' ] (* superscripts *) | '\132' ['\128'-'\191'] | '\133' ['\128'-'\143']) |