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

	Commit message (Collapse)	Author	Age	Files	Lines
*	Update the vendored Flocq library to version 3.4.2	Xavier Leroy	2021-09-25	2	-34/+16
\| \| \| \|	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	13	-241/+883
\|
*	Upgrade embedded version of Flocq to 3.1.	Guillaume Melquiond	2019-03-27	15	-2292/+2434
\| \| \| \| \| \| \| \| \| \| \| \|	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).
*	Upgrade Flocq to version 2.6.1 from upstream (#71)	Xavier Leroy	2018-04-25	3	-138/+118
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	We were previously at 2.5.2. Quoting the NEWS from upstream: Version 2.6.1: - ensured compatibility from Coq 8.4 to 8.8 Version 2.6.0: - ensured compatibility from Coq 8.4 to 8.7 - removed some hypotheses on some lemmas of Fcore_ulp - added lemmas to Fprop_plus_error - improved examples Also: in preparation for Coq 8.8, silence warning "compatibility-notation" when building Flocq, because this warning is on by default in 8.8, and Flocq triggers it a lot.
*	Change Implicit Arguments to Arguments (#225)	Jasper Hugunin	2018-03-28	1	-5/+5
\| \| \| \| \| \| \|	Implicit Arguments is deprecated in Coq since 8.6 or so. Some Implicit Arguments remained in Flocq but were recently changed to Arguments. Apply the same change to our local copy of Flocq. As a positive consequence, we no longer need to suppress the deprecation warnings while compiling Flocq.
*	Adapt proofs to future handling of literal constants in Coq.	Guillaume Melquiond	2017-03-08	7	-69/+58
\| \| \| \| \| \|	This commit is mainly a squash of the relevant compatibility commits from Flocq's master. Most of the changes are meant to make the proofs oblivious to the way constants such as 0, 1, 2, and -1 are represented.
*	Update Flocq to version 2.5.2	Xavier Leroy	2017-02-13	5	-125/+86
\| \| \| \|	This version of Flocq is compatible with Coq 8.6
*	The contradiction tactic has become more powerful.	Maxime Dénès	2017-01-09	1	-2/+1
\|
*	Upgrade to Flocq 2.5.0.	Guillaume Melquiond	2015-09-22	12	-829/+2180
\| \| \| \|	Note: this version of Flocq is compatible with both Coq 8.4 and 8.5.
*	Upgrade to flocq 2.4.0	Jacques-Henri Jourdan	2014-10-07	6	-98/+942
\|
*	Merge of Flocq version 2.2.0.	xleroy	2013-08-02	14	-28/+432
\| \| \| \| \| \| \|	More precise modeling of NaNs. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2303 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Use Flocq for floats	xleroy	2012-06-28	14	-0/+10487
	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1939 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e