compcert - CompCert fork with minor modifications for Vericert.

	Commit message (Collapse)	Author	Age	Files	Lines
*	Use the LGPL instead of the GPL for dual-licensed files	Xavier Leroy	2021-05-08	1	-4/+5
\| \| \| \| \| \|	The GPL makes sense for whole applications, but the dual-licensed Coq and OCaml files are more like libraries to be combined with other code, so the LGPL is more appropriate.
*	Replace `omega` tactic with `lia`	Xavier Leroy	2020-12-29	1	-130/+130
\| \| \| \| \| \| \| \| \| \| \|	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`.
*	Remove useless parameters in theorems int_round_odd_bits and int_round_odd_le	Xavier Leroy	2020-12-29	1	-5/+5
\| \| \| \| \| \| \| \| \|	IEEE754_extra: clear unused context so that none of the context is picked up by tactics and ends as extra parameters to theorems int_round_odd_bits and int_round_odd_le Floats: simplify uses of int_round_odd_bits and int_round_odd_le accordingly.
*	Support the use of already-installed MenhirLib and Flocq libraries	Xavier Leroy	2020-09-21	1	-2/+2
\| \| \| \|	configure flags -use-external-Flocq and -use external-MenhirLib.
*	Rename Fappli_IEEE_extra.v into IEEE754_extra.v	Xavier Leroy	2019-04-26	1	-0/+1515
	To match the new module names from version 3 of Flocq. Plus, it's shorter.