diff options
author | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2021-04-23 18:29:20 +0200 |
---|---|---|
committer | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2021-04-23 18:29:20 +0200 |
commit | bb5dab84859088d70074444cfbf0e51f14e3c782 (patch) | |
tree | 6d9245fc919aa615324025a3976d60646b4fac89 /x86 | |
parent | e4542668e6d348e0300e76bb77105af24aff4233 (diff) | |
download | compcert-bb5dab84859088d70074444cfbf0e51f14e3c782.tar.gz compcert-bb5dab84859088d70074444cfbf0e51f14e3c782.zip |
Move `$` notation in submodule `ClightNotations` and scope `clight_scope`
This avoids a nasty conflict with Ltac2 notations as reported in #392.
The old `$` notation in scope `string_scope` was not used yet, AFAIK.
The new submodule and the new scope are the right places to add future
notations to facilitate working with the output of clightgen.
Fixes: #392
Diffstat (limited to 'x86')
0 files changed, 0 insertions, 0 deletions