aeneas - aeneas rust verifier with a hacky Isabelle backend

	Commit message (Collapse)	Author	Age	Files	Lines
*	Automatically generate the Makefile and _CoqProject files in the tests ↵	Son Ho	2022-11-16	2	-4/+5
\| \| \| \|	subdirectories
*	Generate record field projectors for Coq	Son Ho	2022-11-16	3	-34/+19
\|
*	Change the name of the generated Coq modules	Son Ho	2022-11-16	3	-12/+12
\|
*	Improve formatting	Son Ho	2022-11-16	7	-273/+304
\|
*	Make minor modifications to the extraction	Son Ho	2022-11-16	1	-2/+0
\|
*	Extract the Polonius examples in Coq	Son Ho	2022-11-14	2	-1/+43
\|
*	Regenerate the files and fix the proofs	Son Ho	2022-11-14	4	-59/+71
\|
*	Improve the formatting of [if then else] expressions	Son Ho	2022-11-14	2	-86/+70
\|
*	Reactivate the option -test-trans-unis for Coq	Son Ho	2022-11-14	1	-0/+3
\|
*	Improve the formatting of the generated code	Son Ho	2022-11-14	3	-16/+35
\|
*	Implement a pass to decompose nested patterns in let-bindings	Son Ho	2022-11-14	1	-2/+3
\|
*	Make minor modifications	Son Ho	2022-11-14	1	-2/+1
\|
*	Make good progress on the Coq backend	Son Ho	2022-11-14	9	-0/+1425