diff options
| author | Xavier Leroy <xavier.leroy@inria.fr> | 2016-09-17 14:59:11 +0200 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@inria.fr> | 2016-09-17 14:59:11 +0200 |
| commit | 6b87278c399332f67a4b40958ea2386bb3c1c66e (patch) | |
| tree | dc8961306b936e005165b9dad628051c79eda284 /cfrontend/Cexec.v | |
| parent | 365ba9bd749f060e3ff9287b3283f0157d848557 (diff) | |
| download | compcert-6b87278c399332f67a4b40958ea2386bb3c1c66e.tar.gz compcert-6b87278c399332f67a4b40958ea2386bb3c1c66e.zip | |
Decidableplus: remove stuff that was cut-and-paste from Coq 8.5 library
The cut-and-paste was for compatibility with Coq 8.4
Diffstat (limited to 'cfrontend/Cexec.v')
0 files changed, 0 insertions, 0 deletions