summaryrefslogtreecommitdiff
Commit message (Expand)AuthorAgeFilesLines
...
| * | | 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
* | | | Simplify collapse_ctxAymeric Fromherz2024-05-271-6/+5
generated by cgit v1.2.3 (git 2.25.1) at 2025-04-22 10:24:55 +0000