| Commit message (Collapse) | Author | Age |
|---|
| | |
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
A non-ASCII char is now converted to _UUxxxx_ with xxxx being its unicode index
in hexa. And any preexisting _UU substring in the ident is converted to _UUU.
The switch from __Uxxxx_ to _UUxxxx_ is cosmetic, it just helps the extraction
(less __ in names). But the other part of the patch (detection of preexisting
_UU substrings) is critical to make ascii_of_ident truly injective and avoid
the following kind of proof of False via native_compute :
Definition α := 1.
Definition __U03b1_ := 2.
Lemma oups : False.
Proof.
assert (α = __U03b1_). { native_compute. reflexivity. }
discriminate.
Qed.
|
| |\ |
|
| | |
| |
| |
| |
| |
| |
| | |
Printing invalid UTF-8 string startled GTK too much, leading to CoqIDE dying
improperly. We now check that all strings outputed by Coq are proper UTF-8.
This is not perfect, as CoqIDE will sometimes truncate strings which contains
the null character, but at least it should not crash.
|
| |/ |
|
| |
|
|
|
|
| |
Since type variables are local to the definition, we simply rename
them in case of unicode chars. We also get rid of any ' to avoid
Ocaml illegal 'a' type var (clash with char litteral).
|
| |
|
|
|
|
| |
All superscript numbers are now symbols instead of parts of identifiers.
This disallows some identifiers, but hopefully not a lot of people were
using superscripts as part of identifiers, weren't they?
|
| |
|
|
|
|
| |
with OCaml 3.12.1).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16787 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
| |
Workaround. Some characters seems to be missing in
Camomile's category tables. We add them manually.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16755 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15818 85f007b7-540e-0410-9357-904b9bb8a0f7
|
Pierre-Marie Pédrot
Pierre Letouzey
Matej Kosik
xclerc
regisgia
letouzey