summaryrefslogtreecommitdiff
Commit message (Expand)AuthorAgeFilesLines
...
| * | | fix generated fileNadrieril2024-05-241-1/+1
* | | | Merge pull request #194 from AeneasVerif/afromher/recursive_projectorsSon HO2024-05-245-69/+106
|\ \ \ \ | |/ / / |/| | |
| * | | Update an .opam fileSon Ho2024-05-241-1/+1
| * | | Factor out the code for Lean and CoqSon Ho2024-05-241-143/+41
| * | | Merge branch 'main' into afromher/recursive_projectorsSon Ho2024-05-24147-8592/+10661
| |\ \ \ | |/ / / |/| | |
* | | | Merge pull request #204 from AeneasVerif/test-harness4Guillaume Boisseau2024-05-2469-1379/+1480
|\ \ \ \
| * | | | Update test outputsNadrieril2024-05-2451-1219/+1219
| * | | | runner: Pass options in special commentsNadrieril2024-05-2417-82/+150
| * | | | Fix running individual testsNadrieril2024-05-241-3/+7
| * | | | runner: define an Input moduleNadrieril2024-05-241-90/+92
| * | | | runner: Strongly typed Backend enumNadrieril2024-05-243-62/+89
|/ / / /
* | | | Merge pull request #203 from AeneasVerif/son/duneSon HO2024-05-241-1/+1
|\ \ \ \
| * | | | Downgrade the version of duneSon Ho2024-05-241-1/+1
| | * | | Regenerate Lean files for betreeAymeric Fromherz2024-05-231-0/+4
| | * | | Add simp, reducible attributes to generated Lean projectorsAymeric Fromherz2024-05-231-0/+10
| | * | | Regenerate Lean files for betree following extraction changesAymeric Fromherz2024-05-232-47/+46
| | * | | Do not expand field projector for recursive structs to a let binding in LeanAymeric Fromherz2024-05-231-5/+0
| | * | | Improve formatting of Lean struct projectorsAymeric Fromherz2024-05-231-2/+6
| | * | | Add printing of projectors for recursive structs in Lean backendAymeric Fromherz2024-05-231-3/+130
| | | * | feat: add small pieces of max theoryRyan Lahfa2024-05-241-0/+39
| | |/ / | |/| |
| | | * Improve collapse_ctxSon Ho2024-06-041-1/+42
| | | * Do more cleanupSon Ho2024-06-041-40/+44
| | | * Factor out the code in collapse_ctxSon Ho2024-06-042-153/+56
| | | * Start factoring out the code of reduce_ctx and collapse_ctxSon Ho2024-06-041-91/+162
| | | * Improve merge_abstractions by splitting the markers before mergingSon Ho2024-06-041-0/+75
| | | * Cleanup merge_abstractionsSon Ho2024-06-041-96/+183
| | | * Add a testSon Ho2024-06-034-103/+123
| | | * Fix an issue with the type of the values given back by loopsSon Ho2024-06-033-157/+237
| | | * Fix a bug when composing the continuations in eval_statementSon Ho2024-06-034-122/+131
| | | * Change the order in which we merge abstractionsSon Ho2024-06-035-105/+99
| | | * Cleanup a bitSon Ho2024-06-033-44/+53
| | | * Factor out some code and update some commentsSon Ho2024-06-034-166/+173
| | | * Cleanup a bitSon Ho2024-06-034-91/+87
| | | * Make minor modificationsSon Ho2024-06-034-19/+25
| | | * Update some commentsSon Ho2024-06-031-2/+2
| | | * formatAymeric Fromherz2024-05-311-18/+18
| | | * Add documentation to collapseAymeric Fromherz2024-05-311-1/+27
| | | * Regenerate testsAymeric Fromherz2024-05-3113-35/+35
| | | * Add missing reverse when collapsing environmentAymeric Fromherz2024-05-311-2/+1
| | | * Fix unused variables warningsAymeric Fromherz2024-05-312-13/+18
| | | * Regenerate test outputAymeric Fromherz2024-05-3119-108/+2588
| | | * Avoid adding shared loans twice when merging environmentsAymeric Fromherz2024-05-311-5/+28
| | | * Add markers when creating new abstractions because of a join with bottomAymeric Fromherz2024-05-313-48/+63
| | | * Also fix implementation of Join-SharedBorrowAymeric Fromherz2024-05-311-3/+3
| | | * destructure_abs can be called during collapse: markers should be allowedAymeric Fromherz2024-05-301-4/+0
| | | * Correct implementation of Join-MutBorrows: add markers when creating a new ab...Aymeric Fromherz2024-05-301-3/+4
| | | * More lisible sign for proj_right pretty-printingAymeric Fromherz2024-05-301-1/+1
| | | * Implement two phases of loops join + collapseAymeric Fromherz2024-05-3023-2971/+660
| | | * Compute marker information for borrow/loan mapsAymeric Fromherz2024-05-283-50/+73
| | | * Add type and set/map for marker and borrow idAymeric Fromherz2024-05-284-10/+22
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-23 14:34:22 +0000