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

	Commit message (Collapse)	Author	Age	Files	Lines
*	physical equality	David Monniaux	2021-12-03	1	-1/+6
\|
*	Merge remote-tracking branch 'absint/master' into towards_3.10	David Monniaux	2021-12-01	1	-20/+52
\| \| \| \|	Mostly changes in PTree
*	option monad tactic	Sylvain Boulmé	2021-11-06	1	-19/+8
\|
*	fix compil for coq 8.13.2	Léo Gourdin	2021-09-02	1	-2/+1
\|
*	remove todos, clean	Léo Gourdin	2021-07-28	1	-19/+1
\|
*	non trapping loads	Léo Gourdin	2021-07-23	1	-9/+6
\|
*	branches expansions support	Léo Gourdin	2021-07-22	1	-11/+12
\|
*	expansions btl proofs	Léo Gourdin	2021-07-21	1	-1/+5
\|
*	op simplify BTL intro	Léo Gourdin	2021-07-20	1	-9/+7
\|
*	proof for symbolic simu, need to finish equiv_inputs	Léo Gourdin	2021-07-20	1	-10/+19
\|
*	Finish implem proof, need to adapt scheduler proof	Léo Gourdin	2021-07-19	1	-109/+315
\|
*	hrexec_correct1	Léo Gourdin	2021-07-08	1	-25/+48
\|
*	some progress in canonbuilding	Léo Gourdin	2021-07-07	1	-14/+106
\|
*	symbolic_simu impl definitions	Léo Gourdin	2021-07-07	1	-47/+9
\|
*	hrexec1	Léo Gourdin	2021-07-07	1	-27/+81
\|
*	progress in simulation test	Léo Gourdin	2021-07-07	1	-57/+250
\|
*	Some advance, need to finish canonbuilding proofs	Léo Gourdin	2021-07-06	1	-13/+270
\|
*	lemma on HC_set_reg	Léo Gourdin	2021-07-05	1	-52/+154
\|
*	red_PTree lemmas	Léo Gourdin	2021-07-01	1	-10/+71
\|
*	cbranch expanse	Léo Gourdin	2021-06-30	1	-0/+25
\|
*	coercions and simplify	Léo Gourdin	2021-06-30	1	-2/+90
\|
*	some advance	Léo Gourdin	2021-06-30	1	-14/+154
\|
*	Starting symbolic execution implementation	Léo Gourdin	2021-06-30	1	-0/+314