aboutsummaryrefslogtreecommitdiffstats
path: root/aarch64/Asmgenproof1.v
Commit message (Collapse)AuthorAgeFilesLines
* Asmgenproof1: useless unfolding in proof scripts causing "omega" to failXavier Leroy2019-09-111-3/+3
| | | | "omega" fails in Coq 8.7, but not in 8.8 and later.
* AArch64 portXavier Leroy2019-08-081-0/+1836
This commit adds a back-end for the AArch64 architecture, namely ARMv8 in 64-bit mode.