aboutsummaryrefslogtreecommitdiffstats
path: root/extraction
diff options
context:
space:
mode:
authorDavid Monniaux <david.monniaux@univ-grenoble-alpes.fr>2020-04-22 08:53:06 +0200
committerDavid Monniaux <david.monniaux@univ-grenoble-alpes.fr>2020-04-22 08:53:06 +0200
commit05a5825ee55227327ba1b09a548e3b9ba876d0cf (patch)
tree81bd7ff060ff4d514acc5a98c4d61fcc00357878 /extraction
parentf5da5188171962d13b9f3eac04845dd19d0aa931 (diff)
downloadcompcert-kvx-05a5825ee55227327ba1b09a548e3b9ba876d0cf.tar.gz
compcert-kvx-05a5825ee55227327ba1b09a548e3b9ba876d0cf.zip
use cbn in T instead of simpl in T
Diffstat (limited to 'extraction')
0 files changed, 0 insertions, 0 deletions