aboutsummaryrefslogtreecommitdiff
path: root/plugins/extraction
AgeCommit message (Expand)Author
2012-11-13Added a CString module.ppedrot
2012-10-30Extraction Implicit: consider the parameters of a constructor (fix #2905)letouzey
2012-10-30Extraction: avoid initial strange empty comments after Arnaud's hackletouzey
2012-10-30Fix Separate extraction when a module-as-file is aliased (#2917)letouzey
2012-10-02Remove some more "open" and dead code thanks to OCaml4 warningsletouzey
2012-09-18More cleanup of Util: utf8 aspects moved to a new file unicode.mlletouzey
2012-09-18Cleaning interface of Util.ppedrot
2012-09-17More cleaning on Utils and CList. Some parts of the code beingppedrot
2012-09-15Some documentation and cleaning of CList and Util interfaces.ppedrot
2012-09-14As r15801: putting everything from Util.array_* to CArray.*.ppedrot
2012-09-14Moving Utils.list_* to a proper CList module, which includes stdlibppedrot
2012-09-14This patch removes unused "open" (automatically generated fromregisgia
2012-09-14The new ocaml compiler (4.00) has a lot of very cool warnings,regisgia
2012-08-24Fix Extraction Implicit on axioms.aspiwack
2012-08-24Experimental support for a comment in the files' preamble in extraction.aspiwack
2012-08-24Add option Set/Unset Extraction Conservative Types.aspiwack
2012-08-08Updating headers.herbelin
2012-08-06Vecnacentries.dump_global silently ignores exceptionspboutill
2012-08-05Dump references in Extractionpboutill
2012-08-05Dump referencespboutill
2012-07-05Extraction: Hashtbl.replace uses less ressources than Hashtbl.add (fix #2824)letouzey
2012-07-05ZArith + other : favor the use of modern names instead of compat notationsletouzey
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 17:59:22 +0000