aboutsummaryrefslogtreecommitdiff
path: root/plugins/extraction
AgeCommit message (Expand)Author
2013-05-30bwaa, a Pervasive.comparepboutill
2013-05-12Removing Gmap from Extraction pluginppedrot
2013-05-12Use the Hook module here and there.ppedrot
2013-04-29Splitting Term into five unrelated interfaces:ppedrot
2013-04-22code simplifications concerning Summaryletouzey
2013-03-18Extraction AccessOpaque is now activated again by default (#2952)letouzey
2013-03-15Extract_env : correct exceptions mentionned in a try ... withletouzey
2013-03-13Restrict (try...with...) to avoid catching critical exn (part 9)letouzey
2013-03-13Restrict (try...with...) to avoid catching critical exn (part 6)letouzey
2013-02-26kernel/declarations becomes a pure mliletouzey
2013-02-26Names: shortcuts for building {kn, constant, mind} with empty sectionsletouzey
2013-02-26Names: Modularize constant and mutual_inductiveletouzey
2013-02-19Dir_path --> DirPathletouzey
2013-02-19Classops : avoid some use of Gmapletouzey
2013-02-18use List.rev_map whenever possibleletouzey
2013-02-18Extraction: same as commit 16203, hopefully without NotASort exnsletouzey
2013-02-14Fix extraction of inductive types that Coq auto-detects to be in Propletouzey
2013-01-28Uniformization of the "anomaly" command.ppedrot
2012-12-19Array.create is deprecatedpboutill
2012-12-18Modulification of nameppedrot
2012-12-18Modulification of mod_bound_idppedrot
2012-12-18Modulification of Labelppedrot
2012-12-18Extraction: qualified names in Extract Constant examples (fix #2878)letouzey
2012-12-17Extraction of projections: restrict a hack to ocaml only (fix #2941)letouzey
2012-12-14Modulification of dir_pathppedrot
2012-12-14Modulification of identifierppedrot
2012-12-14Moved Intset and Intmap to Int namespace.ppedrot
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 18:05:47 +0000