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

	Commit message (Collapse)	Author	Age	Files	Lines
*	Adding a BTL record to help oracles	Léo Gourdin	2021-05-19	1	-3/+3
\|
*	start RTL -> BTL	Sylvain Boulmé	2021-05-06	1	-0/+50
\|
*	clean deprecated comments	Sylvain Boulmé	2021-05-05	1	-6/+1
\|
*	Factorize as suggested for call/tailcall	Léo Gourdin	2021-05-04	1	-43/+43
\|
*	finishing proofs and cleanup	Léo Gourdin	2021-05-04	1	-134/+48
\|
*	some advance and simplifications	Léo Gourdin	2021-05-04	1	-67/+71
\|
*	suggestions...	Sylvain Boulmé	2021-05-04	1	-20/+70
\|
*	builtin case OK, call and tailcall started but not finished	Léo Gourdin	2021-05-04	1	-1/+29
\|
*	one example case on main proof	Léo Gourdin	2021-05-04	1	-18/+20
\|
*	Some try in step_simulation	Léo Gourdin	2021-05-04	1	-3/+20
\|
*	proof for Icond in iblock_istep	Léo Gourdin	2021-05-04	1	-1/+31
\|
*	essai avec le cond_star_step	Sylvain Boulmé	2021-05-04	1	-12/+45
\|
*	essais	Sylvain Boulmé	2021-05-03	1	-16/+31
\|
*	some advance	Léo Gourdin	2021-05-03	1	-8/+39
\|
*	Merge branch 'BTL' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert ↵	Sylvain Boulmé	2021-05-03	1	-35/+22
\|\ \| \| \| \| \| \|	into BTL
\| *	A better structure for inductive prop	Léo Gourdin	2021-05-03	1	-35/+25
\| \|
* \|	une autre suggestion	Sylvain Boulmé	2021-05-03	1	-0/+14
\|/
*	Trying a inductive predicate for BTL-RTL proof	Léo Gourdin	2021-05-03	1	-10/+41
\|
*	debroussaillage et precisions...	Sylvain Boulmé	2021-05-01	1	-8/+58
\|
*	BTLtoRTL: proof for internal/external/return states	Léo Gourdin	2021-04-30	1	-0/+25
\|
*	start the new "BTL" IR.	Sylvain Boulmé	2021-04-28	1	-0/+127