aboutsummaryrefslogtreecommitdiffstats
path: root/common
diff options
context:
space:
mode:
authorDavid Monniaux <David.Monniaux@univ-grenoble-alpes.fr>2021-12-13 18:56:49 +0100
committerDavid Monniaux <David.Monniaux@univ-grenoble-alpes.fr>2021-12-13 18:56:49 +0100
commita90018e65444bcd7a4c85ddd815d315cd852e120 (patch)
treef2941391474225246a2b8c04a8bd489d023dd801 /common
parentd85683086bed8b76580616306166965079a02fb3 (diff)
downloadcompcert-kvx-a90018e65444bcd7a4c85ddd815d315cd852e120.tar.gz
compcert-kvx-a90018e65444bcd7a4c85ddd815d315cd852e120.zip
div_approx_reals_correct simplified proof
Diffstat (limited to 'common')
0 files changed, 0 insertions, 0 deletions