aboutsummaryrefslogtreecommitdiff
path: root/plugins/extraction
AgeCommit message (Expand)Author
2012-06-01More cleaningppedrot
2012-06-01Getting rid of Pp.msgnl and Pp.message.ppedrot
2012-05-30Getting rid of Pp.msgppedrot
2012-05-29remove many excessive open Util & Errors in mli'sletouzey
2012-05-29place all files specific to camlp4 syntax extensions in grammar/letouzey
2012-05-29global_reference migrated from Libnames to new Globnames, less deps in gramma...letouzey
2012-03-26Module names and constant/inductive names are now in two separate namespacesletouzey
2012-03-02Noise for nothingpboutill
2011-12-10Extraction: only do the test on generalizable lets for ocamlletouzey
2011-12-08Extraction: avoid internal eta-reduction (fix #2570)letouzey
2011-11-30Extraction: try to avoid issues with an Include directly inside a .vletouzey
2011-11-29Extraction: typo in last commitletouzey
2011-11-28Extraction: Richer patterns in matchs as proposed by P.N. Tollitteletouzey
2011-11-24Added a DEPRECATED flag in declaration of options. For now only two options a...ppedrot
2011-11-02Add type annotations around all calls to Libobject.declare_objectletouzey
2011-09-05Extraction Implicit: fix the numbering of constructor argumentsletouzey
2011-08-25Extraction: allow extraction of records with anonymous fields (fix #2555)letouzey
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 14:23:18 +0000