compcert-kvx - Unnamed repository; edit this file 'description' to name the repository.

	Commit message (Collapse)	Author	Age	Files	Lines
*	Merge branch 'master' into merge_master_8.13.1	Sylvain Boulmé	2021-03-23	1	-12/+12
\|\ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	PARTIAL MERGE (PARTLY BROKEN). See unsolved conflicts in: aarch64/TO_MERGE and riscV/TO_MERGE WARNING: interface of va_args and assembly sections have changed
\| *	Replace `omega` tactic with `lia`	Xavier Leroy	2020-12-29	1	-12/+12
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Since Coq 8.12, `omega` is flagged as deprecated and scheduled for removal. Also replace CompCert's homemade tactics `omegaContradiction`, `xomega`, and `xomegaContradiction` with `lia` and `extlia`. Turn back on the deprecation warning for uses of `omega`. Make the proof of `Ctypes.sizeof_pos` more robust to variations in `lia`.
* \|	non trapping op	David Monniaux	2020-09-30	1	-8/+8
\| \|
* \|	AArch64 division no longer "traps"	David Monniaux	2020-09-30	1	-3/+7
\| \|
* \|	fix compiling for aarch64	David Monniaux	2019-09-20	1	-2/+5
\|/
*	AArch64 port	Xavier Leroy	2019-08-08	1	-0/+764
	This commit adds a back-end for the AArch64 architecture, namely ARMv8 in 64-bit mode.