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

	Commit message (Collapse)	Author	Age	Files	Lines
*	moved stuff to appropriate places and removed irrelevant content	David Monniaux	2022-02-11	1	-0/+18
\|
*	moved functions to a more logical place	David Monniaux	2022-01-13	1	-165/+179
\|
*	progress on lemmas	David Monniaux	2021-12-12	1	-1/+81
\|
*	minor implicit issue	David Monniaux	2021-12-10	1	-2/+2
\|
*	more properties on Znearest	David Monniaux	2021-12-10	1	-2/+35
\|
*	factor proofs	David Monniaux	2021-12-10	1	-1/+20
\|
*	factorize proof	David Monniaux	2021-12-10	1	-28/+22
\|
*	beautify proof	David Monniaux	2021-12-10	1	-24/+16
\|
*	ZofB_ne_correct	David Monniaux	2021-12-10	1	-0/+10
\|
*	ZofB_ne_correct	David Monniaux	2021-12-10	1	-2/+31
\|
*	progress on ZnearestE	David Monniaux	2021-12-10	1	-24/+54
\|
*	ZofB_ne_correct unfinished	David Monniaux	2021-12-08	1	-1/+18
\|
*	Merge branch 'kvx_fp_division' of ↵	David Monniaux	2021-12-07	1	-1/+1
\|\ \| \| \| \| \| \|	gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into kvx_fp_division
\| *	ZnearestE_opp	David Monniaux	2021-12-07	1	-4/+83
\| \|
* \|	ZnearestE_opp	David Monniaux	2021-12-07	1	-3/+121
\|/
*	progress on ZofB_ne	David Monniaux	2021-12-06	1	-0/+51
\|
*	Zdiv_ne	David Monniaux	2021-12-06	1	-0/+11
\|
*	[BROKEN] Merge with v3.9 : something broken for __builtin_expect in ↵	Cyril SIX	2021-06-01	1	-4/+5
\| \| \| \|	cfrontend/C2C.ml
*	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.