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.

0 files changed, 0 insertions, 0 deletions