summaryrefslogtreecommitdiff
path: root/tests/coq/misc (follow)
Commit message (Collapse)AuthorAgeFilesLines
* Bump charon versionNadrieril2024-05-234-6/+6
|
* Regenerate and fix the testsSon Ho2024-04-251-0/+7
|
* Update the tests for ExternalSon Ho2024-04-257-92/+134
|
* Ensure we regenerate files properly in CINadrieril2024-04-182-2/+0
| | | | | Files that weren't regenerated were marked as not automatically-generated.
* Bump charonNadrieril2024-04-171-159/+56
|
* Fix a Coq fileSon Ho2024-04-111-1/+1
|
* Regenerate the test filesSon Ho2024-04-048-185/+165
|
* Regenerate the test filesSon Ho2024-04-047-59/+63
|
* Regenerate the codeSon Ho2024-03-204-22/+17
|
* Regenerate the testsSon Ho2024-03-192-31/+12
|
* Regenerate the test filesSon Ho2024-03-181-18/+18
|
* Regenerate the constants tests and update Primitives/Base.leanSon Ho2024-03-181-18/+35
|
* Update the generated filesSon Ho2024-03-112-31/+32
|
* Regenerate the test filesSon Ho2024-03-091-0/+64
|
* Rename and regenerate some filesSon Ho2024-02-021-1/+1
|
* Regenerate the filesSon Ho2024-01-251-35/+58
|
* Fix an issue in External_FunsExternal.vSon Ho2023-12-231-15/+3
|
* Fix an issue when deconstructing tuples in CoqSon Ho2023-12-231-2/+2
|
* Regenerate the filesSon Ho2023-12-234-38/+22
|
* Improve the micro passes to eliminate pattern `let f := fun x => g x`Son Ho2023-12-231-18/+8
|
* Regenerate the test files and add the fstar-split testsSon Ho2023-12-229-653/+378
|
* Annotate the bound vars in the lambdas for CoqSon Ho2023-12-222-273/+231
|
* Regenerate the test filesSon Ho2023-12-132-61/+75
|
* Regenerate the testsSon Ho2023-12-071-1/+33
|
* Update following changes in CharonSon Ho2023-12-052-74/+132
|
* Regenerate the other filesSon Ho2023-11-292-0/+77
|
* Generate the Bitwise test filesSon Ho2023-11-291-0/+38
|
* Generate a dedicated file for the external typesSon Ho2023-11-2712-24/+59
|
* Update the generation of files for external definitions and regenerate the testsSon Ho2023-11-274-5/+50
|
* Regenerate the filesSon Ho2023-11-218-188/+376
|
* Regenerate most of the test filesSon Ho2023-11-215-54/+60
|
* Regenerate the Coq test filesSon Ho2023-11-095-27/+27
|
* Update the Makefile and regenerate some testsSon Ho2023-11-081-0/+12
|
* Regenerate the Coq test filesSon Ho2023-10-279-514/+802
|
* Regenerate the test files and fix a proofSon Ho2023-09-072-5/+15
|
* Update the nix flake and regenerate the codeSon Ho2023-08-091-1/+1
|
* Regenerate the test filesSon Ho2023-08-081-9/+9
|
* Update the Makefile and regenerate the test filesSon Ho2023-08-049-6/+65
|
* Improve the generated commentsSon Ho2023-07-068-153/+158
|
* Start using namespaces in the Lean backendSon Ho2023-07-051-1/+1
|
* Make good progress on generating code for HOL4Son Ho2023-06-045-64/+60
|
* Start updating simplify_aggregatesSon Ho2023-06-042-7/+7
|
* Make sure let-bindings in Lean end with line breaks and improve formattingSon Ho2023-06-044-21/+39
|
* Improve the pretty names generation for loopsSon Ho2023-02-031-19/+19
|
* Implement a pass to filter the unused input arguments in the loop functionsSon Ho2023-02-031-11/+7
|
* Improve the order of the loop input parametersSon Ho2023-02-031-4/+4
|
* Improve the heuristic to find pretty names for the variables in the loopsSon Ho2023-02-031-69/+69
|
* Regenerate the hashmap code and update the proofsSon Ho2023-02-032-7/+2
|
* Fix some issues with the values given back by loop backward translationsSon Ho2023-02-031-0/+73
|
* Fix an issue with the translation of loops::clearSon Ho2023-02-031-5/+3
|
generated by cgit v1.2.3 (git 2.25.1) at 2024-10-19 23:36:35 +0000