summaryrefslogtreecommitdiff
path: root/tests/coq (follow)
Commit message (Collapse)AuthorAgeFilesLines
* Update the tests for tuplesSon Ho2024-06-111-7/+26
|
* Regenerate the Coq and Lean betreesSon Ho2024-06-051-89/+221
|
* Update charonNadrieril2024-06-059-86/+86
|
* Merge branch 'main' into son/loops2Son Ho2024-06-0432-2144/+586
|\
| * Fix an issue with some names being ignored when generating unique variable namesSon Ho2024-05-281-2/+2
| |
| * Reactivate the infinite-loop.rs testSon Ho2024-05-281-0/+27
| |
| * tests: Rename hashmap_utils -> utilsNadrieril2024-05-283-11/+10
| |
| * Add some testsNadrieril2024-05-281-0/+54
| |
| * tests: Rename betree_main -> betreeNadrieril2024-05-287-84/+84
| |
| * tests: Merge the hashmap test filesNadrieril2024-05-2713-1734/+96
| |
| * Rename some subdirectories for consistencyNadrieril2024-05-249-0/+0
| |
| * Update output filesNadrieril2024-05-248-177/+177
| |
| * Update test outputsNadrieril2024-05-2415-391/+391
| |
* | Add a testSon Ho2024-06-031-34/+39
| |
* | Regenerate testsAymeric Fromherz2024-05-319-31/+31
| |
* | Regenerate test outputAymeric Fromherz2024-05-315-36/+908
| |
* | Implement two phases of loops join + collapseAymeric Fromherz2024-05-305-908/+36
|/
* Tweak a pathNadrieril2024-05-2415-391/+391
|
* Bump charon versionNadrieril2024-05-235-7/+7
|
* Update charonNadrieril2024-04-301-1/+1
|
* Regenerate and fix the testsSon Ho2024-04-259-19/+60
|
* Merge branch 'main' into core-option-unwrapSon Ho2024-04-2513-85/+584
|\
| * Regenerate the Primitives filesSon Ho2024-04-256-0/+450
| |
| * Update the tests for ExternalSon Ho2024-04-257-92/+134
| |
* | Update testsZyad Hassan2024-04-242-14/+0
|/
* 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
|