summaryrefslogtreecommitdiff
path: root/compiler/Config.ml (unfollow)
Commit message (Expand)AuthorFilesLines
2024-03-28WIP Beginning working on better errors: began replacing raise (Failure) and a...Escherichia1-1/+1
2024-03-10Update the name generation and add CLI to print external pat namesSon Ho1-0/+3
2024-03-08Make progress on propagating the changesSon Ho1-44/+0
2024-03-08Remove the option to split fwd/back functions and update SymbolicToPureSon Ho1-63/+0
2024-03-08Update the code generated for tuple projectorsSon Ho1-0/+4
2023-12-21Simplify the type of the merged fwd/back functionsSon Ho1-0/+26
2023-12-21Make good progress on merging the fwd/back functionsSon Ho1-1/+1
2023-12-19Reset Config.return_back_funs to falseSon Ho1-1/+1
2023-12-14Start updating Pure.fun_sig_info to handle merged forward and backward functionsSon Ho1-2/+61
2023-12-13Update Pure.fun_sig_infoSon Ho1-0/+4
2023-12-07Use a better syntax when extracting tuple types (structures with unnamed fields)Son Ho1-1/+17
2023-11-27Fix the issues with the cross-references for OCaml docSon Ho1-1/+1
2023-11-27Update a commentSon Ho1-1/+2
2023-11-27Do not activate the sanity (invariant) checks by defaultSon Ho1-4/+4
2023-11-21Reorganize the "Extract" filesSon Ho1-0/+27
2023-11-09Modify some options and update the MakefileSon Ho1-2/+2
2023-11-09Fix a small issue in AssociatedTypesSon Ho1-3/+3
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-27 03:31:37 +0000