summaryrefslogtreecommitdiff
path: root/compiler/Extract.ml (unfollow)
Commit message (Expand)AuthorFilesLines
2023-12-23Fix an issue when deconstructing tuples in CoqSon Ho1-2/+8
2023-12-22Annotate the bound vars in the lambdas for CoqSon Ho1-20/+36
2023-12-22Fix a minor extraction issueSon Ho1-1/+1
2023-12-22Slightly update the formatting of the do blocksSon Ho1-24/+26
2023-12-21Update the formatting of commentsSon Ho1-8/+6
2023-12-21Remove some asserts which are now uselessSon Ho1-4/+0
2023-12-21Make good progress on merging the fwd/back functionsSon Ho1-1/+3
2023-12-18Do not register the names of the back funs if they are merged with the fwd funsSon Ho1-3/+8
2023-12-15Make progress on propagating the changesSon Ho1-4/+4
2023-12-15Make progress on generalizing the signature informationSon Ho1-4/+4
2023-12-13Update Pure.fun_sig_infoSon Ho1-2/+6
2023-12-07Fix minor issues when extracting a structure with one field as a tupleSon Ho1-21/+34
2023-12-07Use a better syntax when extracting tuple types (structures with unnamed fields)Son Ho1-26/+48
2023-11-24Make a minor fixSon Ho1-1/+1
2023-11-24Update some assumed type names/variantsSon Ho1-6/+1
2023-11-22Improve further the generation of parent clause/trait clause namesSon Ho1-7/+26
2023-11-21Reorganize the "Extract" filesSon Ho1-24/+23
2023-11-21Add span information to the generated codeSon Ho1-12/+19
2023-11-20Use the name matcher implemented in CharonSon Ho1-7/+11
2023-11-16Finish propagating the changes to the names and cleaningSon Ho1-19/+21
2023-11-12Prefix variants related to types with "T"Son Ho1-7/+7
2023-11-12Remove the 'r type variable from the ty type definitionSon Ho1-13/+13
2023-11-09Make the traits work for CoqSon Ho1-140/+251
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 Ho1-9/+29
2023-11-09Fix a small issue in AssociatedTypesSon Ho1-2/+2
2023-11-07Update the extractionSon Ho1-2/+2
2023-11-06Update following some changes in CharonSon Ho1-22/+15
2023-10-26Make progress on fixing the extraction for LeanSon Ho1-1/+1
2023-10-26Fix more issues at extraction and factor out defs in ExtractBuiltinSon Ho1-6/+23
2023-10-25Make the hashmap files typecheck again in LeanSon Ho1-2391/+109
2023-10-25Fix some issues at extraction and add builtinsSon Ho1-23/+22
2023-10-25Update following the addition of raw pointersSon Ho1-1/+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 Ho1-2/+65
2023-10-24Remove the possibility of generating opaque module signaturesSon Ho1-116/+51
2023-10-24Add support for builtin trait implementationsSon Ho1-2/+30
2023-10-24Fix various issues with the builtinsSon Ho1-34/+81
2023-10-23Make progress on handling the builtinsSon Ho1-42/+212
2023-10-23Remove some assumed types and add more support for builtin definitionsSon Ho1-68/+77
2023-10-22Add more support for numeric operations, xor, rotateJonathan Protzenko1-4/+7
2023-10-20Start updating to handle function pointersSon Ho1-2/+2
2023-10-16Improve formatting of scalars in LeanSon Ho1-23/+10
2023-10-13Add supSon Ho1-1/+3
2023-10-06Slightly improve formatting of the generated codeSon Ho1-1/+6
2023-09-22Add Lean extraction of shl/shrAymeric Fromherz1-1/+3
2023-09-19Cleanup a bitSon Ho1-2/+2
2023-09-17Merge trans_ctx and decls_ctxSon Ho1-6/+2
2023-09-17Make progress on correctly extracting trait method callsSon Ho1-26/+84
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-29 17:00:42 +0000