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

	Commit message (Collapse)	Author	Age	Files	Lines
*	big proofs for so / lo	David Monniaux	2019-05-04	1	-0/+18
\|
*	begin add Plq	David Monniaux	2019-05-03	1	-0/+7
\|
*	rm Ofslow	David Monniaux	2019-05-03	1	-1/+1
\|
*	Merge remote-tracking branch 'origin/mppa-work' into mppa-peephole	David Monniaux	2019-05-03	1	-2/+2
\|\
\| *	rm Ofslow (résidu du Risc-V, inutilisé et complique les preuves)	David Monniaux	2019-05-03	1	-2/+2
\| \|
* \|	getting stuck need to move offsets	David Monniaux	2019-05-03	1	-0/+7
\|/
*	it compiles	David Monniaux	2019-05-01	1	-0/+1
\|
*	begin load.xs	David Monniaux	2019-05-01	1	-0/+1
\|
*	Merge remote-tracking branch 'origin/mppa-refactor-reviewed' into mppa-refactor	Cyril SIX	2019-04-08	1	-1/+1
\|\ \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Conflicts: mppa_k1c/Asmblock.v mppa_k1c/Asmblockdeps.v mppa_k1c/PostpassSchedulingproof.v mppa_k1c/lib/Asmblockgenproof0.v
\| *	relecture sylvain	Sylvain Boulmé	2019-04-05	1	-1/+1
\| \| \| \| \| \| \| \|	avec TODOs pour refactoring #90
* \|	#91 Removed completely the duplicated semantics in Asmblock	Cyril SIX	2019-04-05	1	-5/+15
\|/
*	#90 Asmvliw/Asmblock refactoring attempt	Cyril SIX	2019-04-05	1	-3/+3
\|
*	Preuve des load/store registre registre. Reste des modifs mineures dans les ↵	Cyril SIX	2019-04-03	1	-4/+4
\| \| \| \|	preuves de Asmblockdeps
*	Added definition of PLoadRRR and PStoreRRR - no Asmblockgen generation yet	Cyril SIX	2019-04-02	1	-8/+10
\|
*	Plugged Asmblockdeps into PostpassScheduling	Cyril SIX	2019-02-25	1	-1/+7
\|
*	Removing the low_half axiom	Cyril SIX	2019-02-05	1	-4/+4
\|
*	Moved some files to mppa_k1c/lib ; reworked configure and Makefile to allow that	Cyril SIX	2018-11-26	2	-0/+1421