summaryrefslogtreecommitdiff
path: root/tests/coq/misc/External_Funs.v (unfollow)
Commit message (Expand)AuthorFilesLines
2023-12-23Regenerate the filesSon Ho1-3/+1
2023-12-22Regenerate the test files and add the fstar-split testsSon Ho1-68/+27
2023-11-27Generate a dedicated file for the external typesSon Ho1-5/+5
2023-11-27Update the generation of files for external definitions and regenerate the testsSon Ho1-2/+2
2023-11-21Regenerate the filesSon Ho1-9/+18
2023-10-27Regenerate the Coq test filesSon Ho1-19/+20
2023-08-04Update the Makefile and regenerate the test filesSon Ho1-0/+2
2023-07-06Improve the generated commentsSon Ho1-9/+9
2023-06-04Make good progress on generating code for HOL4Son Ho1-4/+4
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
generated by cgit v1.2.3 (git 2.25.1) at 2024-10-19 10:35:35 +0000