diff options
| author | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2020-06-01 11:05:15 +0200 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2020-06-01 11:05:15 +0200 |
| commit | 18859319b1daee0abb32bbc4e89ec5865a6fe082 (patch) | |
| tree | d50056bf5867a7d6b0144a098b18f929e2b90888 /exportclight/Clightgen.ml | |
| parent | 0eba6f63b6bc458d856e477f6f8ec6b78ef78c58 (diff) | |
| download | compcert-kvx-18859319b1daee0abb32bbc4e89ec5865a6fe082.tar.gz compcert-kvx-18859319b1daee0abb32bbc4e89ec5865a6fe082.zip | |
clightgen -short-idents : do not use $"xxx" notation ever
In the original code, collisions could occur: an identifier could
be numbered with a number that happens to be equal to its canonical
encoding. This was harmless but confusing.
Closes: #358
Diffstat (limited to 'exportclight/Clightgen.ml')
0 files changed, 0 insertions, 0 deletions