aboutsummaryrefslogtreecommitdiffhomepage
path: root/tools/coqdoc
diff options
context:
space:
mode:
authorGravatar msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7>2008-06-10 18:28:26 +0000
committerGravatar msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7>2008-06-10 18:28:26 +0000
commite121b1de13ed893a37a73c852e4e9de933eef32a (patch)
tree86522098425c086554fd70638dd622bb3cf138c1 /tools/coqdoc
parent813b9b40ce96c59f9e68b759c876a0ccbfdbf942 (diff)
- Correct handling of DependentMorphism error, using tclFAIL instead of
letting the exception go uncatched. - Reorder definitions in Morphisms, move the PER on (R ==> R') in Morphisms where it can be declared properly. Add an instance for Equivalence => Per. - Change bug#1604 test file to the new semantics of [setoid_rewrite at] - More unicode characters parsed by coqdoc. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11092 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tools/coqdoc')
-rw-r--r--tools/coqdoc/pretty.mll5
1 files changed, 4 insertions, 1 deletions
diff --git a/tools/coqdoc/pretty.mll b/tools/coqdoc/pretty.mll
index a9ad92f4c..d5d8702bc 100644
--- a/tools/coqdoc/pretty.mll
+++ b/tools/coqdoc/pretty.mll
@@ -170,11 +170,14 @@ let firstchar =
['A'-'Z' 'a'-'z' '_'
(* iso 8859-1 accents *)
'\192'-'\214' '\216'-'\246' '\248'-'\255' ] |
+ '\194' '\185' |
(* utf-8 latin 1 supplement *)
'\195' ['\128'-'\191'] |
(* utf-8 letterlike symbols *)
'\206' ['\177'-'\183'] |
- '\226' ('\132' ['\128'-'\191'] | '\133' ['\128'-'\143'])
+ '\226' ('\130' [ '\128'-'\137' ] (* subscripts *)
+ | '\129' [ '\176'-'\187' ] (* superscripts *)
+ | '\132' ['\128'-'\191'] | '\133' ['\128'-'\143'])
let identchar =
firstchar | ['\'' '0'-'9' '@' ]
let id = firstchar identchar*