aboutsummaryrefslogtreecommitdiff
path: root/plugins/extraction/mlutil.ml
AgeCommit message (Expand)Author
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
2012-09-14The new ocaml compiler (4.00) has a lot of very cool warnings,regisgia
2012-08-24Add option Set/Unset Extraction Conservative Types.aspiwack
2012-08-08Updating headers.herbelin
2012-05-29global_reference migrated from Libnames to new Globnames, less deps in gramma...letouzey
2012-03-02Noise for nothingpboutill
2011-12-10Extraction: only do the test on generalizable lets for ocamlletouzey
2011-12-08Extraction: avoid internal eta-reduction (fix #2570)letouzey
2011-11-29Extraction: typo in last commitletouzey
2011-11-28Extraction: Richer patterns in matchs as proposed by P.N. Tollitteletouzey
2011-07-04Extraction: in haskell, __ may have any type, no need to unsafeCoerce itletouzey
2011-04-07Extraction: unfolds the let-in created by Program when handling "match"letouzey
2011-04-07Extraction: avoid some useless Obj.magic by fixing my ML type unifierletouzey
2011-04-03Lazy loading of opaque proofs: fast as -dont-load-proofs without its drawbacksletouzey
2010-12-21Extraction: avoid type-unsafe optimisation of pattern-matchings (fix #2413)letouzey
2010-09-24Dead code in extractionletouzey
2010-09-17Extraction: multiple fixes related with the Not_found encountered by X. Leroyletouzey
2010-07-24Updated all headers for 8.3 and trunkherbelin
2010-07-08Extraction: restrict autoinling to csts whose body is globally visible (fix #...letouzey
2010-07-08Extraction: more factorization of common match branchesletouzey
2010-07-08Extraction: Unset Extraction AutoInline is now the defaultletouzey
2010-06-16Extraction: fix the eta reduction function used in code optimisationsletouzey
2010-06-08Extraction with implicits: perform the occur-check after optimisationsletouzey
2010-05-01Extraction: fix type_expunge_from_sign broken in last commitletouzey
2010-04-30Extraction: an experimental command to get rid of some cst/constructor argumentsletouzey
2010-04-29Remove the svn-specific $Id$ annotationsletouzey
2010-04-16Extraction: restore (temporarily?) a very limited form of linear letin reductionletouzey
2010-04-16Extraction: less eta in calls to global functions, better optimization phaseletouzey
2010-04-16Extraction: improvement of optimizations (kill_dummy, optim_fix)letouzey
2010-04-16Extraction: ad-hoc identifier type with annotations for reductionsletouzey
2010-04-16Extraction: less _ in Haskell (typically for False_rect), less toplevel eta-e...letouzey
2009-10-21This big commit addresses two problems:soubiran
2009-03-20Directory 'contrib' renamed into 'plugins', to end confusion with archive of ...letouzey
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 05:05:12 +0000