summaryrefslogtreecommitdiff
Commit message (Expand)AuthorAgeFilesLines
* `./charon-pin` stores the current charon commitNadrieril2024-05-145-4/+41
* Merge pull request #164 from RaitoBezarius/ofnat_scalarSon HO2024-05-141-0/+5
|\
| * feat(backend/lean): Raw Lean literals can be parsed into scalars automaticallyRyan Lahfa2024-04-301-0/+5
* | Merge pull request #177 from RaitoBezarius/oops-soundness-i-am-sowwySon HO2024-05-141-1/+4
|\ \
| * | backends/lean: repair definition of `core.mem.replace`Ryan Lahfa2024-05-131-1/+4
|/ /
* | Merge pull request #174 from AeneasVerif/bump-charonGuillaume Boisseau2024-05-063-6/+15
|\ \
| * | Update charonNadrieril2024-05-063-6/+15
|/ /
* | Merge pull request #166 from AeneasVerif/afromher/traitsGuillaume Boisseau2024-05-062-4/+7
|\ \
| * \ Merge branch 'main' into afromher/traitsAymeric Fromherz2024-05-064-76/+26
| |\ \ | |/ / |/| |
* | | Merge pull request #173 from AeneasVerif/afromher/docGuillaume Boisseau2024-05-061-1/+1
|\ \ \
| * | | Add menhir and ocamlformat to list of required opam packagesAymeric Fromherz2024-05-061-1/+1
|/ / /
* | | Merge pull request #170 from AeneasVerif/merge-queueGuillaume Boisseau2024-05-031-0/+6
|\ \ \
| * | | Prepare CI for merge queueNadrieril2024-05-031-0/+6
|/ / /
* | | Merge pull request #168 from AeneasVerif/bump-charonGuillaume Boisseau2024-05-021-4/+3
|\ \ \
| * | | Update charonNadrieril2024-05-021-4/+3
|/ / /
* | | Merge pull request #167 from AeneasVerif/bump-charonGuillaume Boisseau2024-05-023-78/+23
|\ \ \
| * | | Update charonNadrieril2024-05-023-78/+23
|/ / /
| * | Update flake.lockAymeric Fromherz2024-05-061-3/+3
| * | Add error when handling mutually recursive traitsAymeric Fromherz2024-05-011-1/+4
|/ /
* | Merge pull request #165 from AeneasVerif/bump-charonGuillaume Boisseau2024-04-307-16/+17
|\ \ | |/ |/|
| * Update charonNadrieril2024-04-307-16/+17
|/
* Merge pull request #159 from zgrannan/add-flake-systemsGuillaume Boisseau2024-04-271-1/+1
|\
| * Use eachDefaultSystem in flake.nix, update charon in flake.lockZack Grannan2024-04-261-1/+1
|/
* Merge pull request #125 from zhassan-aws/core-option-unwrapSon HO2024-04-2636-89/+173
|\
| * Update the decreases clauses for the betreeSon Ho2024-04-262-8/+3
| * Update the F* clauses for the betreeSon Ho2024-04-261-2/+1
| * Update compiler/ExtractBuiltin.mlSon HO2024-04-261-1/+1
| * Update a decreases clauseSon Ho2024-04-261-1/+7
| * Regenerate and fix the testsSon Ho2024-04-2523-51/+140
| * Update the backend and ExtractBuiltin.mlSon Ho2024-04-254-2/+18
| * Merge branch 'main' into core-option-unwrapSon Ho2024-04-2537-238/+1491
| |\
| * | Fix a couple of testsZyad Hassan2024-04-244-13/+4
| * | Update testsZyad Hassan2024-04-247-44/+0
| * | Add core::option::unwrap builtinZyad Hassan2024-04-244-5/+15
* | | Merge pull request #158 from RaitoBezarius/lean-ci-under-nixSon HO2024-04-262-14/+6
|\ \ \ | |_|/ |/| |
| * | chore(ci): move Lean CI under NixRyan Lahfa2024-04-242-14/+6
| |/
* | Merge pull request #135 from RaitoBezarius/option-takeSon HO2024-04-2536-258/+1489
|\ \ | |/ |/|
| * Regenerate the Primitives filesSon Ho2024-04-2513-0/+975
| * Update the flake.lockSon Ho2024-04-251-15/+15
| * Update the tests for ExternalSon Ho2024-04-2520-237/+470
| * Merge branch 'main' into option-takeSon Ho2024-04-2529-605/+523
| |\ | |/ |/|
* | Merge pull request #156 from RaitoBezarius/ordersSon HO2024-04-231-0/+15
|\ \
| * | feat(backends/lean): scalars form a linear orderRyan Lahfa2024-04-231-0/+15
* | | Merge pull request #154 from AeneasVerif/ci-fmtSon HO2024-04-233-2/+23
|\ \ \
| * | | TypoGuillaume Boisseau2024-04-231-1/+1
| * | | ci: Forbid compilation warningsNadrieril2024-04-221-0/+1
| * | | ci: check code formattingNadrieril2024-04-223-2/+22
* | | | Merge pull request #155 from AeneasVerif/dedup-ciSon HO2024-04-231-0/+22
|\ \ \ \ | |/ / / |/| | |
| * | | ci: avoid running duplicate jobsNadrieril2024-04-221-0/+22
|/ / /
* | | Merge pull request #151 from AeneasVerif/son/fix-loops2Son HO2024-04-226-35/+80
|\ \ \