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 /driver | |
| parent | e4542668e6d348e0300e76bb77105af24aff4233 (diff) | |
| download | compcert-kvx-bb5dab84859088d70074444cfbf0e51f14e3c782.tar.gz compcert-kvx-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 'driver')
0 files changed, 0 insertions, 0 deletions