summaryrefslogtreecommitdiff
path: root/tests/coq/misc/External_Funs.v (unfollow)
Commit message (Expand)AuthorFilesLines
2023-02-03Regenerate the hashmap code and update the proofsSon Ho1-4/+1
2023-02-03Regenerate the filesSon Ho1-7/+2
2022-11-16Change the name of the generated Coq modulesSon Ho1-6/+6
2022-11-16Improve formattingSon Ho1-19/+20
2022-11-14Regenerate the files and fix the proofsSon Ho1-1/+1
2022-11-14Reactivate the option -test-trans-unis for CoqSon Ho1-0/+3
2022-11-14Improve the formatting of the generated codeSon Ho1-8/+18
2022-11-14Implement a pass to decompose nested patterns in let-bindingsSon Ho1-2/+3
2022-11-14Make minor modificationsSon Ho1-2/+1
2022-11-14Make good progress on the Coq backendSon Ho1-0/+100