aboutsummaryrefslogtreecommitdiff
path: root/plugins/extraction
AgeCommit message (Expand)Author
2011-07-29Extract_env: generic = on prec_declaration replaced by prec_declaration_equalpuech
2011-07-29Extraction: replace generic = on mutual_inductive_body by mib_equalpuech
2011-07-04Set Extraction KeepSingleton: an option for not decapsulating singleton typesletouzey
2011-07-04Extraction: in haskell, __ may have any type, no need to unsafeCoerce itletouzey
2011-07-04Extraction: in haskell, type signatures for __ and unsafeCoerce (fix #2552)letouzey
2011-07-04Extraction: forbid Prop-polymorphism of inductives when extracting to Ocamlletouzey
2011-05-19Extraction: avoid lots of late mind_of_knletouzey
2011-05-19Extraction: global reference should be indexed on their user part (fix #2540)letouzey
2011-05-18Extraction: avoid printing of Recursive Extraction in coqide's consoleletouzey
2011-05-16Fixed my last patch: these files no longer use nat_beq (automaticallyvsiles
2011-05-11Print Module (Type) M now tries to print more detailsletouzey
2011-05-05Modularization of BinInt, related fixes in the stdlibletouzey
2011-05-05Modularization of BinNat + fixes of stdlibletouzey
2011-05-05Modularization of BinPos + fixes in Stdlibletouzey
2011-05-05Extraction: allow extraction foo when foo is an alias notationletouzey
2011-04-15Extraction: nicer error when a toplevel module has no body (#2525)letouzey
2011-04-15Extraction: allow extracting Ascii.ascii to native Char in Haskell (fix #2515)letouzey
2011-04-13Extraction: opaque terms are not traversed anymore by defaultletouzey
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
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-05 10:36:07 +0000