diff options
author | Pierre Letouzey <pierre.letouzey@inria.fr> | 2016-05-19 15:18:26 +0200 |
---|---|---|
committer | Pierre Letouzey <pierre.letouzey@inria.fr> | 2016-05-19 15:18:26 +0200 |
commit | 244d7a9aafe7ad613dd2095ca3126560cb3ea1d0 (patch) | |
tree | 26102e433f0072ab32f724fa231693510119c37b /proofs | |
parent | c14e6eebc6c3696623a440cd7eaa4a8d8fe4f492 (diff) |
Unicode.ascii_of_ident is now truly injective
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.
Diffstat (limited to 'proofs')
0 files changed, 0 insertions, 0 deletions