aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/extraction/table.ml
Commit message (Expand)AuthorAge
* Lazy loading of opaque proofs: fast as -dont-load-proofs without its drawbacksGravatar letouzey2011-04-03
* Extraction: a warning when an opaque constant is enterredGravatar letouzey2011-03-07
* A new command "Separate Extraction"Gravatar letouzey2011-03-07
* Extraction: avoid type-unsafe optimisation of pattern-matchings (fix #2413)Gravatar letouzey2010-12-21
* Extraction: allow to use Extraction Inline / NoInline even from under a section.Gravatar letouzey2010-10-06
* Dead code in extractionGravatar letouzey2010-09-24
* Some dead code removal, thanks to Oug analyzerGravatar 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: fix a bit the extraction under modulesGravatar letouzey2010-07-15
* Extraction: Unset Extraction AutoInline is now the defaultGravatar letouzey2010-07-08
* Extraction Library Foo creates Foo.ml, not foo.ml (correct version)Gravatar letouzey2010-07-07
* Extraction Library Foo creates Foo.ml, not foo.mlGravatar letouzey2010-07-07
* Extraction: some more work on the (re)naming frameworkGravatar letouzey2010-07-07
* Extraction: (yet another) rework of the renaming codeGravatar letouzey2010-07-05
* Extraction Implicits: can accept argument names instead of just positionsGravatar letouzey2010-06-10
* 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: an experimental command to get rid of some cst/constructor argumentsGravatar letouzey2010-04-30
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* Extraction: ad-hoc identifier type with annotations for reductionsGravatar letouzey2010-04-16
* A bit of cleaning around name generation + creation of dedicated file namegen.mlGravatar herbelin2009-11-09
* This big commit addresses two problems:Gravatar soubiran2009-10-21
* Remove useless Liboject.export_function fieldGravatar glondu2009-09-17
* Death of "survive_module" and "survive_section" (the first one wasGravatar herbelin2009-08-13
* Cleaning of Nametab continued + fixed a compilation bug in previous commit.Gravatar herbelin2009-08-06
* - Cleaning phase of the interfaces of libnames.ml and nametab.mlGravatar herbelin2009-08-06
* Improved parameterization of Coq:Gravatar herbelin2009-08-02
* Directory 'contrib' renamed into 'plugins', to end confusion with archive of ...Gravatar letouzey2009-03-20
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-29 11:51:30 +0000