aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/extraction
Commit message (Expand)AuthorAge
* Module names and constant/inductive names are now in two separate namespacesGravatar letouzey2012-03-26
* 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: try to avoid issues with an Include directly inside a .vGravatar letouzey2011-11-30
* Extraction: typo in last commitGravatar letouzey2011-11-29
* Extraction: Richer patterns in matchs as proposed by P.N. TollitteGravatar letouzey2011-11-28
* Added a DEPRECATED flag in declaration of options. For now only two options a...Gravatar ppedrot2011-11-24
* Add type annotations around all calls to Libobject.declare_objectGravatar letouzey2011-11-02
* Extraction Implicit: fix the numbering of constructor argumentsGravatar letouzey2011-09-05
* Extraction: allow extraction of records with anonymous fields (fix #2555)Gravatar letouzey2011-08-25
* Extract_env: generic = on prec_declaration replaced by prec_declaration_equalGravatar puech2011-07-29
* Extraction: replace generic = on mutual_inductive_body by mib_equalGravatar puech2011-07-29
* Set Extraction KeepSingleton: an option for not decapsulating singleton typesGravatar letouzey2011-07-04
* Extraction: in haskell, __ may have any type, no need to unsafeCoerce itGravatar letouzey2011-07-04
* Extraction: in haskell, type signatures for __ and unsafeCoerce (fix #2552)Gravatar letouzey2011-07-04
* Extraction: forbid Prop-polymorphism of inductives when extracting to OcamlGravatar letouzey2011-07-04
* Extraction: avoid lots of late mind_of_knGravatar letouzey2011-05-19
* Extraction: global reference should be indexed on their user part (fix #2540)Gravatar letouzey2011-05-19
* Extraction: avoid printing of Recursive Extraction in coqide's consoleGravatar letouzey2011-05-18
* Fixed my last patch: these files no longer use nat_beq (automaticallyGravatar vsiles2011-05-16
* Print Module (Type) M now tries to print more detailsGravatar letouzey2011-05-11
* Modularization of BinInt, related fixes in the stdlibGravatar letouzey2011-05-05
* Modularization of BinNat + fixes of stdlibGravatar letouzey2011-05-05
* Modularization of BinPos + fixes in StdlibGravatar letouzey2011-05-05
* Extraction: allow extraction foo when foo is an alias notationGravatar letouzey2011-05-05
* Extraction: nicer error when a toplevel module has no body (#2525)Gravatar letouzey2011-04-15
* Extraction: allow extracting Ascii.ascii to native Char in Haskell (fix #2515)Gravatar letouzey2011-04-15
* Extraction: opaque terms are not traversed anymore by defaultGravatar letouzey2011-04-13
* 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: customized inductives are always standardGravatar glondu2011-03-31
* Extraction: a warning when an opaque constant is enterredGravatar letouzey2011-03-07
* Extraction: fix printing of haskell modular namesGravatar letouzey2011-03-07
* Extraction: avoid printing unused mutual fix components (fix #2477)Gravatar letouzey2011-03-07
* A new command "Separate Extraction"Gravatar letouzey2011-03-07
* Extraction: improved indentation of extracted code (fix #2497)Gravatar letouzey2011-03-04
* Extraction: Add missing parenthesis around emulated pattern-match (fix #2478)Gravatar letouzey2011-02-25
* Fix indentation of default pattern in haskell case (bug #2476)Gravatar letouzey2011-02-25
* A fine-grain control of inlining at functor application via priority levelsGravatar letouzey2011-01-31
* Extraction : fix Extract Inlined Constant for Haskell and Scheme (#2469)Gravatar letouzey2011-01-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: re-introduce some eta-expansions in rare situations leading to '_...Gravatar letouzey2010-09-20
* Extraction: multiple fixes related with the Not_found encountered by X. LeroyGravatar letouzey2010-09-17
* Fix likely semantic typosGravatar glondu2010-09-15
* Fix unescaped end-of-lines (OCaml warning 29)Gravatar glondu2010-09-13
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-28 13:55:38 +0000