aboutsummaryrefslogtreecommitdiff
path: root/plugins/extraction
AgeCommit message (Expand)Author
2014-05-09Reuse universe level substitutions for template polymorphism, fixing performanceMatthieu Sozeau
2014-05-06Fix extraction taking a type in the wrong environment.Matthieu Sozeau
2014-05-06Fix a pervasive equality use.Matthieu Sozeau
2014-05-06- Rename eq to equal in Univ, document new modules, set interfaces.Matthieu Sozeau
2014-05-06Initial work on reintroducing old-style polymorphism for compatibility (the s...Matthieu Sozeau
2014-05-06This commit adds full universe polymorphism and fast projections to Coq.Matthieu Sozeau
2014-03-08Using HMaps in global references.Pierre-Marie Pédrot
2014-03-05Remove many superfluous 'open' indicated by ocamlc -w +33Pierre Letouzey
2014-03-03Fixing Pervasives.equality in extraction.Pierre-Marie Pédrot
2014-02-26Lazyconstr -> OpaqueproofEnrico Tassi
2014-02-26New compilation mode -vi2voEnrico Tassi
2013-10-24More monomorphic List.mem + List.assoc + ...letouzey
2013-10-24Turn many List.assoc into List.assoc_fletouzey
2013-10-23cList.index is now cList.index_f, same for index0letouzey
2013-09-27Removing a bunch of generic equalities.ppedrot
2013-09-19Get rid of the uses of deprecated OCaml elements (still remaining compatible ...xclerc
2013-08-22Nicer code concerning dirpaths and modpath around Libletouzey
2013-08-20Declarations.mli: reorganization of modular structuresletouzey
2013-08-08Vernac classification streamlined (handles VERNAC EXTEND)gareuselesinge
2013-08-08State Transaction Machinegareuselesinge
2013-07-17Lib.contents () instead of Lib.contents_after Noneletouzey
2013-07-17Extraction : message about lack of support for toplevel Includeletouzey
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 22:44:19 +0000