summaryrefslogtreecommitdiff
path: root/compiler/Translate.ml (follow)
Commit message (Expand)AuthorAgeFilesLines
* Remove redundant `llbc_name` fieldNadrieril2024-06-281-4/+5
* Update charonNadrieril2024-06-241-13/+26
* Update charonNadrieril2024-06-211-0/+3
* Deactivate some linter options for the generated Lean filesSon Ho2024-06-171-0/+9
* Implement a BorrowCheck.borrow_check_crateSon Ho2024-06-051-2/+3
* Add an option to run Aeneas as a borrow checkerSon Ho2024-06-051-18/+19
* Remove the options from the functions synthesizing the symbolic ASTSon Ho2024-05-301-3/+2
* Rename meta into spanAymeric Fromherz2024-05-241-14/+14
* Fix a crash which happens when type definitions are ignoredSon Ho2024-05-241-2/+5
* Print the name patterns of the definitions which fail to extractSon Ho2024-05-241-11/+19
* Add error when handling mutually recursive traitsAymeric Fromherz2024-05-011-1/+4
* item_metaNadrieril2024-04-181-3/+3
* Merge remote-tracking branch 'origin/main' into son/cleanSon Ho2024-04-111-20/+73
|\
| * Cleanup a bit and improve the error messagesSon Ho2024-04-071-34/+35
| * Resolved comments and added the name of the not translated elementEscherichia2024-04-051-6/+14
| * resolved commentsEscherichia2024-04-051-7/+16
| * error catching should now be able to tell when code couldn't be generatedEscherichia2024-04-051-11/+46
* | Add field mk_return, mk_panic in SymbolicToPure.bs_ctxSon Ho2024-04-041-0/+2
|/
* Cleanup and fix a mistakeSon Ho2024-03-291-0/+1
* added file and line arg to craise and cassertEscherichia2024-03-291-2/+2
* changes after git rebase mainEscherichia2024-03-281-3/+2
* Should answer all comments, there are still some TODO: error message leftEscherichia2024-03-281-7/+7
* Still need to fill the TODO: error message and check some meta but it buildsEscherichia2024-03-281-24/+24
* WIP: translate.ml and extract.ml do not compile. Some assert left to do and w...Escherichia2024-03-281-25/+25
* WIP: does not compile yet because we need to propagate the meta variable.Escherichia2024-03-281-3/+3
* WIP Beginning working on better errors: began replacing raise (Failure) and a...Escherichia2024-03-281-40/+42
* Make good progress on adding generics to global constantsSon Ho2024-03-181-0/+1
* Fix a minor issueSon Ho2024-03-171-1/+1
* Update the generation of namesSon Ho2024-03-111-1/+1
* Make progress on propagating the changesSon Ho2024-03-081-118/+27
* Update the library for F*Son Ho2023-12-221-1/+7
* Fix several issuesSon Ho2023-12-211-13/+16
* Make good progress on merging the fwd/back functionsSon Ho2023-12-211-1/+2
* Remove SymbolicToPure.bs_ctx.loop_backward_outputsSon Ho2023-12-191-1/+0
* Simplify SymbolicToPure.bs_ctx.{backward_outputs, loop_backward_outputs}Son Ho2023-12-191-16/+1
* Rename some definitionsSon Ho2023-12-181-7/+7
* Make progress on updating the codeSon Ho2023-12-151-114/+93
* Make progress on generated merged fwd/back functionsSon Ho2023-12-141-1/+3
* Update Pure.fun_sig_infoSon Ho2023-12-131-2/+6
* Update following changes in CharonSon Ho2023-12-051-1/+1
* Update the way the Primitives file is copiedSon Ho2023-11-271-13/+20
* Generate a dedicated file for the external typesSon Ho2023-11-271-12/+102
* Update the generation of files for external definitions and regenerate the testsSon Ho2023-11-271-9/+14
* Reorganize the "Extract" filesSon Ho2023-11-211-15/+4
* Use the name matcher implemented in CharonSon Ho2023-11-201-11/+14
* Finish propagating the changes to the names and cleaningSon Ho2023-11-161-81/+78
* Add RegionsHierarchy.mlSon Ho2023-11-131-2/+5
* Remove the 'r type variable from the ty type definitionSon Ho2023-11-121-6/+6
* Make the traits work for CoqSon Ho2023-11-091-6/+16
* Make progress on fixing the extraction for LeanSon Ho2023-10-261-18/+3
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-22 14:53:31 +0000