summaryrefslogtreecommitdiff
path: root/tests/coq/misc (follow)
Commit message (Expand)AuthorAgeFilesLines
* Regenerate the testsSon Ho2024-06-174-5/+5
* Update the tests for tuplesSon Ho2024-06-111-7/+26
* Update charonNadrieril2024-06-056-67/+67
* Merge branch 'main' into son/loops2Son Ho2024-06-049-162/+243
|\
| * Reactivate the infinite-loop.rs testSon Ho2024-05-281-0/+27
| * Add some testsNadrieril2024-05-281-0/+54
| * Update output filesNadrieril2024-05-247-161/+161
| * Update test outputsNadrieril2024-05-247-161/+161
* | Add a testSon Ho2024-06-031-34/+39
* | Regenerate testsAymeric Fromherz2024-05-311-12/+12
* | Regenerate test outputAymeric Fromherz2024-05-311-16/+430
* | Implement two phases of loops join + collapseAymeric Fromherz2024-05-301-430/+16
|/
* Tweak a pathNadrieril2024-05-247-161/+161
* 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
* 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