aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/extraction/mlutil.ml
Commit message (Expand)AuthorAge
* Update copyright headers.Gravatar Maxime Dénès2016-01-20
* Extraction: slightly better heuristic for Obj.magic simplificationsGravatar Pierre Letouzey2015-12-16
* Extraction: fixed beta-red with Obj.magic (#2795 again) + other simplificationsGravatar Pierre Letouzey2015-12-16
* Extraction: fix a few little glitches with my last commit (replacing unused v...Gravatar Pierre Letouzey2015-12-15
* Extraction: replace unused variable names by _ in funs and matchs (fix #2842)Gravatar Pierre Letouzey2015-12-15
* Extraction: allow basic beta-reduction even through a MLmagic (fix #2795)Gravatar Pierre Letouzey2015-12-14
* Extraction: propagate implicit args in inner fixpoint (bug #4243 part 2)Gravatar Pierre Letouzey2015-12-14
* Extraction: nicer implementation of ImplicitsGravatar Pierre Letouzey2015-12-12
* Fix some typos.Gravatar Guillaume Melquiond2015-10-13
* Update headers.Gravatar Maxime Dénès2015-01-12
* "allows to", like "allowing to", is improperGravatar Jason Gross2014-08-25
* Remove many superfluous 'open' indicated by ocamlc -w +33Gravatar Pierre Letouzey2014-03-05
* Fixing Pervasives.equality in extraction.Gravatar Pierre-Marie Pédrot2014-03-03
* More monomorphic List.mem + List.assoc + ...Gravatar letouzey2013-10-24
* Removing a bunch of generic equalities.Gravatar ppedrot2013-09-27
* Get rid of the uses of deprecated OCaml elements (still remaining compatible ...Gravatar xclerc2013-09-19
* Nicer code concerning dirpaths and modpath around LibGravatar letouzey2013-08-22
* Restrict (try...with...) to avoid catching critical exn (part 6)Gravatar letouzey2013-03-13
* kernel/declarations becomes a pure mliGravatar letouzey2013-02-26
* Names: shortcuts for building {kn, constant, mind} with empty sectionsGravatar letouzey2013-02-26
* Dir_path --> DirPathGravatar letouzey2013-02-19
* Modulification of LabelGravatar ppedrot2012-12-18
* Modulification of dir_pathGravatar ppedrot2012-12-14
* Modulification of identifierGravatar ppedrot2012-12-14
* Moved Intset and Intmap to Int namespace.Gravatar ppedrot2012-12-14
* Remove some more "open" and dead code thanks to OCaml4 warningsGravatar letouzey2012-10-02
* Some documentation and cleaning of CList and Util interfaces.Gravatar ppedrot2012-09-15
* As r15801: putting everything from Util.array_* to CArray.*.Gravatar ppedrot2012-09-14
* Moving Utils.list_* to a proper CList module, which includes stdlibGravatar ppedrot2012-09-14
* This patch removes unused "open" (automatically generated fromGravatar regisgia2012-09-14
* The new ocaml compiler (4.00) has a lot of very cool warnings,Gravatar regisgia2012-09-14
* Add option Set/Unset Extraction Conservative Types.Gravatar aspiwack2012-08-24
* Updating headers.Gravatar herbelin2012-08-08
* global_reference migrated from Libnames to new Globnames, less deps in gramma...Gravatar letouzey2012-05-29
* Noise for nothingGravatar pboutill2012-03-02
* Extraction: only do the test on generalizable lets for ocamlGravatar letouzey2011-12-10
* Extraction: avoid internal eta-reduction (fix #2570)Gravatar letouzey2011-12-08
* Extraction: typo in last commitGravatar letouzey2011-11-29
* Extraction: Richer patterns in matchs as proposed by P.N. TollitteGravatar letouzey2011-11-28
* Extraction: in haskell, __ may have any type, no need to unsafeCoerce itGravatar letouzey2011-07-04
* Extraction: unfolds the let-in created by Program when handling "match"Gravatar letouzey2011-04-07
* Extraction: avoid some useless Obj.magic by fixing my ML type unifierGravatar letouzey2011-04-07
* Lazy loading of opaque proofs: fast as -dont-load-proofs without its drawbacksGravatar letouzey2011-04-03
* Extraction: avoid type-unsafe optimisation of pattern-matchings (fix #2413)Gravatar letouzey2010-12-21
* Dead code in extractionGravatar letouzey2010-09-24
* Extraction: multiple fixes related with the Not_found encountered by X. LeroyGravatar letouzey2010-09-17
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
* Extraction: restrict autoinling to csts whose body is globally visible (fix #...Gravatar letouzey2010-07-08
* Extraction: more factorization of common match branchesGravatar letouzey2010-07-08
* Extraction: Unset Extraction AutoInline is now the defaultGravatar letouzey2010-07-08