aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/extraction/mlutil.mli
Commit message (Expand)AuthorAge
* Remove (useless) aliases from the API.Gravatar Matej Košík2017-06-10
* Put all plugins behind an "API".Gravatar Matej Kosik2017-06-07
* Update copyright headers.Gravatar Maxime Dénès2016-01-20
* Extraction: replace unused variable names by _ in funs and matchs (fix #2842)Gravatar Pierre Letouzey2015-12-15
* Extraction: nicer implementation of ImplicitsGravatar Pierre Letouzey2015-12-12
* Update headers.Gravatar Maxime Dénès2015-01-12
* 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
* Modulification of nameGravatar ppedrot2012-12-18
* Modulification of identifierGravatar ppedrot2012-12-14
* Updating headers.Gravatar herbelin2012-08-08
* remove many excessive open Util & Errors in mli'sGravatar letouzey2012-05-29
* 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: Richer patterns in matchs as proposed by P.N. TollitteGravatar letouzey2011-11-28
* 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: more factorization of common match branchesGravatar letouzey2010-07-08
* Extraction with implicits: perform the occur-check after optimisationsGravatar letouzey2010-06-08
* Extract Inductive is now possible toward non-inductive types (e.g. nat => int)Gravatar letouzey2010-05-21
* Extraction: fix type_expunge_from_sign broken in last commitGravatar letouzey2010-05-01
* Extraction: an experimental command to get rid of some cst/constructor argumentsGravatar letouzey2010-04-30
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* Extraction: less eta in calls to global functions, better optimization phaseGravatar letouzey2010-04-16
* Extraction: ad-hoc identifier type with annotations for reductionsGravatar letouzey2010-04-16
* This big commit addresses two problems:Gravatar soubiran2009-10-21
* Directory 'contrib' renamed into 'plugins', to end confusion with archive of ...Gravatar letouzey2009-03-20