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

	Commit message (Expand)	Author	Age	Files	Lines
*	[BROKEN] Merge with v3.9 : something broken for __builtin_expect in cfrontend...	Cyril SIX	2021-06-01	1	-13/+14
*	replacing omega with lia in some file	Léo Gourdin	2021-03-29	1	-1/+2
*	Merge branch 'master' into merge_master_8.13.1	Sylvain Boulmé	2021-03-23	1	-31/+31
\|\
\| *	Replace `omega` tactic with `lia`	Xavier Leroy	2020-12-29	1	-31/+31
* \|	CSE2 alias analysis for Risc-V	David Monniaux	2020-03-03	1	-0/+7
\|/
*	Refine the type of function results in AST.signature	Xavier Leroy	2020-02-21	1	-9/+15
*	Move Z definitions out of Integers and into Zbits	Xavier Leroy	2019-04-26	1	-4/+5
*	lib/Coqlib.v: remove defns about multiplication, division, modulus	Xavier Leroy	2019-04-23	1	-2/+2
*	Replace nat_of_Z with Z.to_nat	Xavier Leroy	2019-04-23	1	-1/+1
*	Remove coq warnings (#28)	Bernhard Schommer	2017-09-22	1	-25/+25
*	Hybrid 64bit/32bit PowerPC port	Bernhard Schommer	2017-05-03	1	-1/+1
*	Support for 64-bit architectures: generic support	Xavier Leroy	2016-10-01	1	-45/+75
*	Updated PR by removing whitespaces. Bug 17450.	Bernhard Schommer	2015-10-20	1	-117/+117
*	Long-overdue renaming: val_inject -> Val.inject, etc, for consistency with Va...	Xavier Leroy	2015-04-30	1	-10/+10
*	Merge of "newspilling" branch:	xleroy	2014-07-23	1	-239/+290
*	- Back to origins: suppress Mfloat64al32 chunk and align Mfloat64 to 4.	xleroy	2014-01-12	1	-15/+8
*	Introduce and use the platform-specific Archi module giving:	xleroy	2014-01-03	1	-14/+13
*	Merge of the float32 branch:	xleroy	2013-05-19	1	-1/+1
*	Big merge of the newregalloc-int64 branch. Lots of changes in two directions:	xleroy	2013-04-20	1	-5/+159
*	Glasnost: making transparent a number of definitions that were opaque	xleroy	2013-03-10	1	-0/+1
*	lib/Integers.v: revised and extended, faster implementation based on	xleroy	2013-02-10	1	-17/+18
*	Integers: specialized function to compute x mod 2^N; used in "repr" to	xleroy	2012-12-21	1	-1/+2
*	- Revised non-overflow constraints on memory injections so that	xleroy	2012-07-23	1	-9/+35
*	Memdata: cleanup continued	xleroy	2012-05-26	1	-178/+105
*	CSE: add recognition of some combined operators, conditions, and addressing m...	xleroy	2012-05-26	1	-298/+149
*	Merge of the nonstrict-ops branch:	xleroy	2012-01-14	1	-16/+0
*	Cleaned up old commented-out parts	xleroy	2011-08-19	1	-8/+0
*	Back from Oregon commit.	xleroy	2011-07-05	1	-5/+8
*	Integers: cleaned up bitwise operations, redefined shr, zero_ext and sign_ext	xleroy	2010-08-21	1	-50/+32
*	Support for inlined built-ins.	xleroy	2010-06-29	1	-13/+0
*	Fewer float axioms.	xleroy	2010-05-09	1	-2/+1
*	Revised encoding/decoding of floats	xleroy	2010-05-09	1	-165/+182
*	Copyright notice	xleroy	2010-03-12	1	-0/+18
*	Merge of the newmem and newextcalls branches:	xleroy	2010-03-07	1	-0/+1058