aboutsummaryrefslogtreecommitdiff
path: root/plugins/extraction
AgeCommit message (Expand)Author
2011-04-03Lazy loading of opaque proofs: fast as -dont-load-proofs without its drawbacksletouzey
2011-03-31Extraction: customized inductives are always standardglondu
2011-03-07Extraction: a warning when an opaque constant is enterredletouzey
2011-03-07Extraction: fix printing of haskell modular namesletouzey
2011-03-07Extraction: avoid printing unused mutual fix components (fix #2477)letouzey
2011-03-07A new command "Separate Extraction"letouzey
2011-03-04Extraction: improved indentation of extracted code (fix #2497)letouzey
2011-02-25Extraction: Add missing parenthesis around emulated pattern-match (fix #2478)letouzey
2011-02-25Fix indentation of default pattern in haskell case (bug #2476)letouzey
2011-01-31A fine-grain control of inlining at functor application via priority levelsletouzey
2011-01-07Extraction : fix Extract Inlined Constant for Haskell and Scheme (#2469)letouzey
2010-12-21Extraction: avoid type-unsafe optimisation of pattern-matchings (fix #2413)letouzey
2010-10-06Extraction: allow to use Extraction Inline / NoInline even from under a section.letouzey
2010-09-24Dead code in extractionletouzey
2010-09-24Some dead code removal, thanks to Oug analyzerletouzey
2010-09-20Extraction: re-introduce some eta-expansions in rare situations leading to '_...letouzey
2010-09-17Extraction: multiple fixes related with the Not_found encountered by X. Leroyletouzey
2010-09-15Fix likely semantic typosglondu
2010-09-13Fix unescaped end-of-lines (OCaml warning 29)glondu
2010-07-24Updated all headers for 8.3 and trunkherbelin
2010-07-15Extraction: fix a bit the extraction under modulesletouzey
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-07-07Extraction Library Foo creates Foo.ml, not foo.ml (correct version)letouzey
2010-07-07Extraction Library Foo creates Foo.ml, not foo.mlletouzey
2010-07-07Extraction: get advantage of nicer, algebraic, module typesletouzey
2010-07-07Extraction: some more work on the (re)naming frameworkletouzey
2010-07-05Extraction: (yet another) rework of the renaming codeletouzey
2010-07-02Extraction: better support of modulesletouzey
2010-07-02Extraction: no more MPself hence no need for subst during ppletouzey
2010-06-28Extraction: handling modules (not functors) in Haskell by name manglingletouzey
2010-06-28Extraction: remove a useless matchletouzey
2010-06-23Extraction: nicer simple extraction of custom defs (fix #2204)letouzey
2010-06-21Extraction: replace unicode characters in ident by ascii encodings (fix #2158...letouzey
2010-06-16Extraction: fix the eta reduction function used in code optimisationsletouzey
2010-06-15Extraction: in support library, more and nicer big_intletouzey
2010-06-10Extraction Implicits: can accept argument names instead of just positionsletouzey
2010-06-08Extraction with implicits: perform the occur-check after optimisationsletouzey
2010-06-08Typo in ExtrOcamlString: list char instead of char listletouzey
2010-06-04Extraction: attempt to provide nice extraction of chars and strings for Ocamlletouzey
2010-06-04Extraction: finish ExtrOcamlNatInt, add similar translation nat==>big_intletouzey
2010-06-02Extraction: start of a support libraryletouzey
2010-05-21Extract Inductive is now possible toward non-inductive types (e.g. nat => int)letouzey
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: cosmetics when using ocaml + Extract Inductive to symbolsletouzey
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-08 23:23:09 +0000