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

	Commit message (Collapse)	Author	Age	Files	Lines
*	finishing RTLtoBTL	Léo Gourdin	2021-05-17	1	-23/+34
\|
*	mib lemma	Léo Gourdin	2021-05-17	1	-26/+29
\|
*	Lemmas on ISTEP	Léo Gourdin	2021-05-17	1	-194/+126
\|
*	some advance	Léo Gourdin	2021-05-16	1	-24/+191
\|
*	iblock_istep rec and correct lemmas	Léo Gourdin	2021-05-13	1	-0/+83
\|
*	ascii simu	Léo Gourdin	2021-05-12	1	-17/+48
\|
*	finish proof	Léo Gourdin	2021-05-11	1	-39/+45
\|
*	new lemma definition, some preparations in existing proofs	Léo Gourdin	2021-05-11	1	-52/+65
\|
*	new strong_state predicate and lemma	Léo Gourdin	2021-05-10	1	-38/+72
\|
*	Some more proof cases, comments and cleanup	Léo Gourdin	2021-05-10	1	-29/+96
\|
*	is_exp and bcond proof	Léo Gourdin	2021-05-10	1	-18/+35
\|
*	Merge branch 'BTL' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert ↵	Léo Gourdin	2021-05-09	1	-0/+2
\|\ \| \| \| \| \| \|	into BTL
\| *	idee pour simplifier la preuve: restreindre le "right_assoc" en "expand" !	Sylvain Boulmé	2021-05-08	1	-0/+2
\| \|
* \|	mib_exit draft	Léo Gourdin	2021-05-09	1	-3/+4
\| \|
* \|	Some advance in proof and NOTRAP loads fix	Léo Gourdin	2021-05-07	1	-4/+53
\| \|
* \|	intermediate lemma for opt_simu intro case	Léo Gourdin	2021-05-07	1	-10/+21
\|/
*	a draft for the Bnop case	Léo Gourdin	2021-05-07	1	-11/+25
\|
*	proof OK for Call and Return states	Léo Gourdin	2021-05-07	1	-6/+21
\|
*	starting RTL->BTL proof	Léo Gourdin	2021-05-06	1	-4/+46
\|
*	fix match_states	Sylvain Boulmé	2021-05-06	1	-6/+8
\|
*	cleaner match_states	Sylvain Boulmé	2021-05-06	1	-16/+21
\|
*	start RTL -> BTL	Sylvain Boulmé	2021-05-06	1	-0/+239