Extraction: replace unicode characters in ident by ascii encodings (fix #2158,#2179)

 Any unicode character above 128 is replaced by __Uxxxx_ where xxxx is
 the hexa code for the unicode index of this character. For instance
 <alpha> is turned into __U03b1_. I know, this is ugly. Better
 solutions are welcome, but I'm afraid we can't do much better as long
 as ocaml and haskell don't accept unicode letters in idents. At
 least, this way we're pretty sure this translating won't create name
 conflit, as long as extraction users avoid __ in their names,
 something that they should already do btw (see for instance
 extraction of coinductive types in ocaml). Yes, I should add a test
 and a warning/error in case of use of __ someday.

 NB: this commit belongs proudly to the quick'n'dirty category

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13173 85f007b7-540e-0410-9357-904b9bb8a0f7

0 files changed, 0 insertions, 0 deletions