compcert - CompCert fork with minor modifications for Vericert.

	Commit message (Collapse)	Author	Age	Files	Lines
*	Upgrade Flocq to 4.1.1	Xavier Leroy	2023-03-10	1	-2/+2
\|
*	Upgrade to Flocq 4.1.	Guillaume Melquiond	2022-04-26	1	-34/+39
\|
*	Upgrade to Flocq 4.0.	Guillaume Melquiond	2022-04-25	1	-8/+35
\|
*	Update the vendored Flocq library to version 3.4.2	Xavier Leroy	2021-09-25	1	-2/+2
\| \| \| \|	For compatibility with the upcoming Coq 8.14.
*	Replace `omega` tactic with `lia`	Xavier Leroy	2020-12-29	1	-1/+1
\| \| \| \| \| \| \| \| \| \| \|	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`.
*	Update Flocq to 3.4.0 (#383)	Guillaume Melquiond	2020-12-28	1	-10/+22
\|
*	Upgrade embedded version of Flocq to 3.1.	Guillaume Melquiond	2019-03-27	1	-0/+2402
	Main changes to CompCert outside of Flocq are as follows: - Minimal supported version of Coq is now 8.7, due to Flocq requirements. - Most modifications are due to Z2R being dropped in favor of IZR and to the way Flocq now handles NaNs. - CompCert now correctly handles NaNs for the Risc-V architecture (hopefully).