aboutsummaryrefslogtreecommitdiffstats
path: root/exportclight
diff options
context:
space:
mode:
authorJason Gross <jasongross9@gmail.com>2018-01-17 15:40:12 +0100
committerXavier Leroy <xavierleroy@users.noreply.github.com>2018-01-17 15:40:12 +0100
commit7d3440a69c3a344613b11e7fe4b5f20a655d177f (patch)
tree4359ce9940bb77d3e92b0677c09b5645d0a252cd /exportclight
parent51a10cf84b2d762b9f83b7387c022294423b3b78 (diff)
downloadcompcert-kvx-7d3440a69c3a344613b11e7fe4b5f20a655d177f.tar.gz
compcert-kvx-7d3440a69c3a344613b11e7fe4b5f20a655d177f.zip
Don't depend on the judgmental behavior of Bool.eqb (#217)
This change is backwards compatible, and makes flocq compatible with https://github.com/coq/coq/pull/6596. Was applied to the Flocq master sources https://gitlab.inria.fr/flocq/flocq/commit/db356aa5ea0fd0234e3872f70e8972086055cd57
Diffstat (limited to 'exportclight')
0 files changed, 0 insertions, 0 deletions