summaryrefslogtreecommitdiff
path: root/compiler (unfollow)
Commit message (Expand)AuthorFilesLines
2023-11-13Add RegionsHierarchy.mlSon Ho16-147/+453
2023-11-12Add the "V" prefix to most variants related to valuesSon Ho15-645/+629
2023-11-12Prefix variants related to types with "T"Son Ho27-321/+320
2023-11-12Rename some variantsSon Ho9-15/+15
2023-11-12Remove the 'r type variable from the ty type definitionSon Ho42-1811/+1305
2023-11-09Make the traits work for CoqSon Ho6-193/+353
2023-11-09Extract the trait parent clauses after the types and the constantsSon Ho1-24/+25
2023-11-09Progress on making the traits work for F*Son Ho3-36/+115
2023-11-09Modify some options and update the MakefileSon Ho2-9/+9
2023-11-09Fix a small issue in AssociatedTypesSon Ho7-15/+21
2023-11-07Update the extractionSon Ho1-2/+2
2023-11-07Update the normalization of associated typesSon Ho4-50/+126
2023-11-06Fix a naming issueSon Ho1-1/+3
2023-11-06Fix some issues when extracting references to SelfSon Ho1-30/+57
2023-11-06Update following some changes in CharonSon Ho4-57/+59
2023-10-30Make minor updates following changes in CharonSon Ho2-6/+2
2023-10-27Fix minor issues in the name collision detectionSon Ho2-10/+23
2023-10-27Fix a minor issue and regenerate some F* test filesSon Ho1-9/+20
2023-10-26Make minor modifications and update the array test for F*Son Ho3-14/+17
2023-10-26Fix some issues and regenerate the HashmapMain example for LeanSon Ho3-7/+18
2023-10-26Improve the handling of saved function effects in ExtractBuiltin.mlSon Ho2-24/+44
2023-10-26Make progress on fixing the extractionSon Ho1-8/+24
2023-10-26Improve ExtractBuiltin.mlSon Ho2-46/+57
2023-10-26Make progress on fixing the extraction for LeanSon Ho4-106/+130
2023-10-26Fix more issues at extraction and factor out defs in ExtractBuiltinSon Ho2-266/+166
2023-10-25Make the hashmap files typecheck again in LeanSon Ho7-2740/+2667
2023-10-25Fix some issues at extraction and add builtinsSon Ho4-38/+340
2023-10-25Fix some issues to make the array test succeed againSon Ho2-16/+44
2023-10-25Remove the warning for loopsSon Ho1-8/+0
2023-10-25Update following the addition of raw pointersSon Ho12-17/+77
2023-10-24Handle properly the builtin, non fallible functionsSon Ho3-18/+54
2023-10-24Start taking into account non-fallible functions like core::mem::replaceSon Ho2-5/+15
2023-10-24Fix minor issuesSon Ho1-4/+4
2023-10-24Fix an issue coming from the modification for the opaque signaturesSon Ho1-12/+7
2023-10-24Fix a printing issue with scalar valuesSon Ho1-3/+5
2023-10-24Filter some type arguments for the builtin types/functionsSon Ho4-10/+87
2023-10-24Remove the possibility of generating opaque module signaturesSon Ho4-330/+111
2023-10-24Add support for builtin trait implementationsSon Ho4-20/+80
2023-10-24Fix various issues with the builtinsSon Ho4-122/+234
2023-10-24Add some debugging informationSon Ho1-0/+7
2023-10-23Make progress on handling the builtinsSon Ho4-154/+270
2023-10-23Remove some assumed types and add more support for builtin definitionsSon Ho24-808/+763
2023-10-22Add more support for numeric operations, xor, rotateJonathan Protzenko2-7/+28
2023-10-20Start updating to handle function pointersSon Ho16-100/+163
2023-10-16Improve formatting of scalars in LeanSon Ho1-23/+10
2023-10-16Fix a small issueSon Ho2-13/+53
2023-10-13Add supSon Ho6-3/+23
2023-10-06Slightly improve formatting of the generated codeSon Ho1-1/+6
2023-09-19Cleanup a bitSon Ho2-12/+12
2023-09-17Normalize the function signatures before translation to pureSon Ho9-150/+294
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-24 01:55:26 +0000