diff options
| author | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2021-01-21 16:07:24 +0100 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2021-01-21 16:07:24 +0100 |
| commit | eca149363d20d94198a4b1e1ae4f9f964e468098 (patch) | |
| tree | 5b8573ab8114b5aabd308aa65e834934c1961b94 /powerpc | |
| parent | ab62e1bed37d2efe4d2a9e0139839bae21b1cdd9 (diff) | |
| download | compcert-kvx-eca149363d20d94198a4b1e1ae4f9f964e468098.tar.gz compcert-kvx-eca149363d20d94198a4b1e1ae4f9f964e468098.zip | |
Define `fold_ind_aux` and `fold_ind` transparently
The extraction mechanism wants to extract them (because they are in
Type, probably). The current opaque definition causes a warning at
extraction-time.
Diffstat (limited to 'powerpc')
0 files changed, 0 insertions, 0 deletions