aboutsummaryrefslogtreecommitdiff
path: root/plugins/extraction/mlutil.ml
AgeCommit message (Expand)Author
2019-11-21[coq] Untabify the whole ML codebase.Emilio Jesus Gallego Arias
2019-11-01Add extraction for primitive floatsErik Martin-Dorel
2019-09-04Merge PR #10577: Fix #7348: extraction of dependent record projectionsMaxime Dénès
2019-08-10[extraction] Fix #7191: Avoid unsound eta-reductionKazuhiko Sakaguchi
2019-07-31Fix #7348: extraction of dependent record projectionsKazuhiko Sakaguchi
2019-07-08[api] Deprecate GlobRef constructors.Emilio Jesus Gallego Arias
2019-06-17Update ml-style headers to new year.Théo Zimmermann
2019-02-04Primitive integersMaxime Dénès
2018-05-23Collecting List.smart_* functions into a module List.Smart.Hugo Herbelin
2018-05-23Collecting Array.smart_* functions into a module Array.Smart.Hugo Herbelin
2018-05-04[api] Rename `global_reference` to `GlobRef.t` to follow kernel style.Emilio Jesus Gallego Arias
2018-02-27Update headers following #6543.Théo Zimmermann
2017-10-06Merge PR #1118: Extraction : minor support stuff for the new Extraction Compu...Maxime Dénès
2017-10-05Extraction: reduce eta-redexes whose cores are atomic (solves indirectly BZ#4...Pierre Letouzey
2017-10-04Extraction : minor support stuff for the new Extraction Compute pluginPierre Letouzey
2017-07-25Extraction: do not mix Haskell types Any and () (revert 8e257d4, fix bugs 484...Pierre Letouzey
2017-07-17[API] Remove `open API` in ml files in favor of `-open API` flag.Emilio Jesus Gallego Arias
2017-07-04Bump year in headers.Pierre-Marie Pédrot
2017-06-10Remove (useless) aliases from the API.Matej Košík
2017-06-07Put all plugins behind an "API".Matej Kosik
2016-01-20Update copyright headers.Maxime Dénès
2015-12-16Extraction: slightly better heuristic for Obj.magic simplificationsPierre Letouzey
2015-12-16Extraction: fixed beta-red with Obj.magic (#2795 again) + other simplificationsPierre Letouzey
2015-12-15Extraction: fix a few little glitches with my last commit (replacing unused v...Pierre Letouzey
2015-12-15Extraction: replace unused variable names by _ in funs and matchs (fix #2842)Pierre Letouzey
2015-12-14Extraction: allow basic beta-reduction even through a MLmagic (fix #2795)Pierre Letouzey
2015-12-14Extraction: propagate implicit args in inner fixpoint (bug #4243 part 2)Pierre Letouzey
2015-12-12Extraction: nicer implementation of ImplicitsPierre Letouzey
2015-10-13Fix some typos.Guillaume Melquiond
2015-01-12Update headers.Maxime Dénès
2014-08-25"allows to", like "allowing to", is improperJason Gross
2014-03-05Remove many superfluous 'open' indicated by ocamlc -w +33Pierre Letouzey
2014-03-03Fixing Pervasives.equality in extraction.Pierre-Marie Pédrot
2013-10-24More monomorphic List.mem + List.assoc + ...letouzey
2013-09-27Removing a bunch of generic equalities.ppedrot
2013-09-19Get rid of the uses of deprecated OCaml elements (still remaining compatible ...xclerc
2013-08-22Nicer code concerning dirpaths and modpath around Libletouzey
2013-03-13Restrict (try...with...) to avoid catching critical exn (part 6)letouzey
2013-02-26kernel/declarations becomes a pure mliletouzey
2013-02-26Names: shortcuts for building {kn, constant, mind} with empty sectionsletouzey
2013-02-19Dir_path --> DirPathletouzey
2012-12-18Modulification of Labelppedrot
2012-12-14Modulification of dir_pathppedrot
2012-12-14Modulification of identifierppedrot
2012-12-14Moved Intset and Intmap to Int namespace.ppedrot
2012-10-02Remove some more "open" and dead code thanks to OCaml4 warningsletouzey
2012-09-15Some documentation and cleaning of CList and Util interfaces.ppedrot
2012-09-14As r15801: putting everything from Util.array_* to CArray.*.ppedrot
2012-09-14Moving Utils.list_* to a proper CList module, which includes stdlibppedrot
2012-09-14This patch removes unused "open" (automatically generated fromregisgia
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 21:47:21 +0000