aboutsummaryrefslogtreecommitdiffstats
path: root/extraction
diff options
context:
space:
mode:
authorSylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr>2020-11-18 11:37:03 +0100
committerSylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr>2020-11-18 11:37:03 +0100
commite042d77cbd7d1f24459d08b26b521dbc0c7ac71d (patch)
tree50c77c6fc7382ad575155b40e5fdbff0f53826ab /extraction
parent917179f4f3889fd3c233d8c156184ab92102bf51 (diff)
downloadcompcert-kvx-e042d77cbd7d1f24459d08b26b521dbc0c7ac71d.tar.gz
compcert-kvx-e042d77cbd7d1f24459d08b26b521dbc0c7ac71d.zip
CLEAN THE PREVIOUS COMMIT !
By default: restore the initial behavior of abstractbb/ImpSimuTest In order to print the dump: set the boolean FULL_DEBUG_DUMP (at the top of the file) to true. And recompile Coq files.
Diffstat (limited to 'extraction')
0 files changed, 0 insertions, 0 deletions