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 /cparser/Machine.ml | |
parent | ab62e1bed37d2efe4d2a9e0139839bae21b1cdd9 (diff) | |
download | compcert-eca149363d20d94198a4b1e1ae4f9f964e468098.tar.gz compcert-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 'cparser/Machine.ml')
0 files changed, 0 insertions, 0 deletions