summaryrefslogtreecommitdiff
path: root/tests/coq/misc (follow)
Commit message (Collapse)AuthorAgeFilesLines
* Update charonNadrieril2024-06-284-6/+6
|
* Update charonNadrieril2024-06-242-2/+2
|
* Bump charonNadrieril2024-06-181-5/+5
|
* Update charonNadrieril2024-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
| | | | | 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
|