summaryrefslogtreecommitdiff
path: root/tests/coq (follow)
Commit message (Collapse)AuthorAgeFilesLines
* Regenerate the Primitives filesSon Ho2024-04-256-0/+450
|
* Update the tests for ExternalSon Ho2024-04-257-92/+134
|
* Ensure we regenerate files properly in CINadrieril2024-04-186-6/+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-0420-535/+501
|
* Regenerate the test filesSon Ho2024-04-042-12/+12
|
* Regenerate the test filesSon Ho2024-04-0413-99/+104
|
* Regenerate the codeSon Ho2024-03-209-126/+119
|
* Regenerate the testsSon Ho2024-03-199-64/+26
|
* Update the demoSon Ho2024-03-191-10/+38
|
* Regenerate the test filesSon Ho2024-03-182-22/+114
|
* Regenerate the constants tests and update Primitives/Base.leanSon Ho2024-03-181-18/+35
|
* Regenerate the test filesSon Ho2024-03-113-83/+78
|
* Update the generated filesSon Ho2024-03-115-128/+134
|
* Regenerate the test filesSon Ho2024-03-092-0/+133
|
* Add some missing filesSon Ho2024-02-092-0/+30
|
* Add some demo filesSon Ho2024-02-092-0/+1066
|
* Rename and regenerate some filesSon Ho2024-02-025-119/+119
|
* Regenerate the filesSon Ho2024-01-252-66/+80
|
* 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-239-91/+47
|
* 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-2222-2666/+1731
|
* Annotate the bound vars in the lambdas for CoqSon Ho2023-12-222-273/+231
|
* Regenerate the test filesSon Ho2023-12-137-61/+95
|
* Regenerate the testsSon Ho2023-12-072-16/+39
|
* Update following changes in CharonSon Ho2023-12-053-97/+155
|
* Regenerate the other filesSon Ho2023-11-297-0/+457
|
* Generate the Bitwise test filesSon Ho2023-11-291-0/+38
|
* Regenerate the testsSon Ho2023-11-291-29/+42
|
* Regenerate the test filesSon Ho2023-11-291-5/+0
|
* Generate a dedicated file for the external typesSon Ho2023-11-2728-54/+151
|
* Update the generation of files for external definitions and regenerate the testsSon Ho2023-11-2712-16/+136
|
* Regenerate the filesSon Ho2023-11-241-8/+2
|
* Regenerate the test filesSon Ho2023-11-221-45/+62
|
* Regenerate the filesSon Ho2023-11-211-27/+31
|
* Regenerate the filesSon Ho2023-11-2118-478/+956
|
* Regenerate the betree filesSon Ho2023-11-212-58/+58
|
* Regenerate the Traits filesSon Ho2023-11-211-60/+66
|
* Regenerate most of the test filesSon Ho2023-11-2113-383/+425
|
* Regenerate the Coq test filesSon Ho2023-11-0914-80/+1403
|
* Update the Makefile and regenerate some testsSon Ho2023-11-081-0/+12
|
* Add some files for the Coq trait testsSon Ho2023-10-272-0/+28
|
* Regenerate the Coq test filesSon Ho2023-10-2723-2117/+3588
|
* Regenerate the test files and fix a proofSon Ho2023-09-079-23/+75
|
* Regenerate the array testsSon Ho2023-08-181-0/+9
|
* Add tests which use const generics as valuesSon Ho2023-08-181-0/+4
|
* Update the nix flake and regenerate the codeSon Ho2023-08-094-4/+4
|