summaryrefslogtreecommitdiff
path: root/compiler/Config.ml (unfollow)
Commit message (Expand)AuthorFilesLines
2023-10-24Remove the possibility of generating opaque module signaturesSon Ho1-7/+0
2023-09-14Make progress on the extractionSon Ho1-0/+4
2023-09-13Fix more issuesSon Ho1-0/+8
2023-08-31Make progress on Extract and ExtractBaseSon Ho1-0/+8
2023-08-04Add an option to not override Hashmap.leanSon Ho1-0/+8
2023-07-06Use short names for the structure fields in LeanSon Ho1-0/+11
2023-07-05Start using namespaces in the Lean backendSon Ho1-0/+7
2023-07-04Reorganize the Lean testsSon Ho1-0/+5
2023-06-04Make good progress on generating code for HOL4Son Ho1-2/+3
2023-06-04Add a special expression for structure creation/updateSon Ho1-1/+0
2023-06-04Consistently use the names TerminationMeasure and DecreasesProofSon Ho1-7/+16
2023-06-04Initial Lean backend, WIPJonathan Protzenko1-3/+3
2023-02-03Fix the comments for ocamldocSon Ho1-1/+1
2023-02-03Implement a micro-pass to simplify the let-bindings followed by a returnSon Ho1-1/+1
2023-02-03Make progress on the fixed point computationSon Ho1-1/+1
2023-02-03Start implementing support for loopsSon Ho1-3/+15
2022-11-16Generate record field projectors for CoqSon Ho1-5/+3
2022-11-14Add a `-use-fuel` optionSon Ho1-1/+5
2022-11-14Implement a pass to decompose nested patterns in let-bindingsSon Ho1-2/+19
2022-11-14Make good progress on the Coq backendSon Ho1-3/+64
2022-11-14Reorganize the project to prepare for new backendsSon Ho1-2/+3
2022-11-11Fix some issues with the commentsSon Ho1-7/+7
2022-11-10Implement a Config.ml file which groups all the global options in referencesSon Ho1-0/+192
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-29 13:45:30 +0000