aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/extraction
Commit message (Expand)AuthorAge
* More monomorphic List.mem + List.assoc + ...Gravatar letouzey2013-10-24
* Turn many List.assoc into List.assoc_fGravatar letouzey2013-10-24
* cList.index is now cList.index_f, same for index0Gravatar letouzey2013-10-23
* Removing a bunch of generic equalities.Gravatar ppedrot2013-09-27
* Get rid of the uses of deprecated OCaml elements (still remaining compatible ...Gravatar xclerc2013-09-19
* Nicer code concerning dirpaths and modpath around LibGravatar letouzey2013-08-22
* Declarations.mli: reorganization of modular structuresGravatar letouzey2013-08-20
* Vernac classification streamlined (handles VERNAC EXTEND)Gravatar gareuselesinge2013-08-08
* State Transaction MachineGravatar gareuselesinge2013-08-08
* Lib.contents () instead of Lib.contents_after NoneGravatar letouzey2013-07-17
* Extraction : message about lack of support for toplevel IncludeGravatar letouzey2013-07-17
* bwaa, a Pervasive.compareGravatar pboutill2013-05-30
* Removing Gmap from Extraction pluginGravatar ppedrot2013-05-12
* Use the Hook module here and there.Gravatar ppedrot2013-05-12
* Splitting Term into five unrelated interfaces:Gravatar ppedrot2013-04-29
* code simplifications concerning SummaryGravatar letouzey2013-04-22
* Extraction AccessOpaque is now activated again by default (#2952)Gravatar letouzey2013-03-18
* Extract_env : correct exceptions mentionned in a try ... withGravatar letouzey2013-03-15
* Restrict (try...with...) to avoid catching critical exn (part 9)Gravatar letouzey2013-03-13
* Restrict (try...with...) to avoid catching critical exn (part 6)Gravatar letouzey2013-03-13
* kernel/declarations becomes a pure mliGravatar letouzey2013-02-26
* Names: shortcuts for building {kn, constant, mind} with empty sectionsGravatar letouzey2013-02-26
* Names: Modularize constant and mutual_inductiveGravatar letouzey2013-02-26
* Dir_path --> DirPathGravatar letouzey2013-02-19
* Classops : avoid some use of GmapGravatar letouzey2013-02-19
* use List.rev_map whenever possibleGravatar letouzey2013-02-18
* Extraction: same as commit 16203, hopefully without NotASort exnsGravatar letouzey2013-02-18
* Fix extraction of inductive types that Coq auto-detects to be in PropGravatar letouzey2013-02-14
* Uniformization of the "anomaly" command.Gravatar ppedrot2013-01-28
* Array.create is deprecatedGravatar pboutill2012-12-19
* Modulification of nameGravatar ppedrot2012-12-18
* Modulification of mod_bound_idGravatar ppedrot2012-12-18
* Modulification of LabelGravatar ppedrot2012-12-18
* Extraction: qualified names in Extract Constant examples (fix #2878)Gravatar letouzey2012-12-18
* Extraction of projections: restrict a hack to ocaml only (fix #2941)Gravatar letouzey2012-12-17
* Modulification of dir_pathGravatar ppedrot2012-12-14
* Modulification of identifierGravatar ppedrot2012-12-14
* Moved Intset and Intmap to Int namespace.Gravatar ppedrot2012-12-14
* Added a CString module.Gravatar ppedrot2012-11-13
* Extraction Implicit: consider the parameters of a constructor (fix #2905)Gravatar letouzey2012-10-30
* Extraction: avoid initial strange empty comments after Arnaud's hackGravatar letouzey2012-10-30
* Fix Separate extraction when a module-as-file is aliased (#2917)Gravatar letouzey2012-10-30
* Remove some more "open" and dead code thanks to OCaml4 warningsGravatar letouzey2012-10-02
* More cleanup of Util: utf8 aspects moved to a new file unicode.mlGravatar letouzey2012-09-18
* Cleaning interface of Util.Gravatar ppedrot2012-09-18
* More cleaning on Utils and CList. Some parts of the code beingGravatar ppedrot2012-09-17
* Some documentation and cleaning of CList and Util interfaces.Gravatar ppedrot2012-09-15
* As r15801: putting everything from Util.array_* to CArray.*.Gravatar ppedrot2012-09-14
* Moving Utils.list_* to a proper CList module, which includes stdlibGravatar ppedrot2012-09-14
* This patch removes unused "open" (automatically generated fromGravatar regisgia2012-09-14