| Age | Commit message (Collapse) | Author |
|---|
|
The warning was pointless since the notation was accepted and parsed
anyway.
We now treat unrecognized unicode characters like ordinary
undefined tokens (e.g. "#" in a bare Coq).
For instance, "aₚ", or ".ₚ", or "?ₚ" now fail with "Undefined token"
rather than "Unsupported Unicode character".
|
|
|
|
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
|
