diff options
| author | msozeau | 2008-05-15 12:51:59 +0000 |
|---|---|---|
| committer | msozeau | 2008-05-15 12:51:59 +0000 |
| commit | 4c3301517cf8887b3684fda58e2e4626a072a5fb (patch) | |
| tree | bd1ed746e255a9f25b486711163001b2f45d8017 /lib | |
| parent | a8b034513e0c03ceb7e154949b15f62ac6862f3b (diff) | |
Various fixes:
- Fix a typo in lowercase_utf8
- Fix generation of signatures in subtac_cases not working for dependent
inductive types with dependent indices.
- Fix coercion of inductive types generating ill-typed terms.
- Fix test script using new syntax for Instances.
- Move simpl_existTs to Program.Equality and use it in simpl_depind.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10932 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/util.ml | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/lib/util.ml b/lib/util.ml index c1cd931119..af99e2b233 100644 --- a/lib/util.ml +++ b/lib/util.ml @@ -350,7 +350,9 @@ let lowercase_utf8 s unicode = | 0x038C -> 0x03CC | x when 0x038E <= x & x <= 0x038F -> x + 63 | x when 0x0390 <= x & x <= 0x03AB & x <> 0x03A2 -> x + 32 - | x when 0x03AC <= x & x <= 0x039E -> + (* utf-8 Greek lowercase letters U03B0-03CE *) + | x when 0x03AC <= x & x <= 0x03CE -> x + | x when 0x03CF <= x & x <= 0x03FF -> warning ("Unable to decide which lowercase letter to map to "^s); x (* utf-8 Cyrillic letters U0400-0481 *) | x when 0x0400 <= x & x <= 0x040F -> x + 80 |