| Commit message (Expand) | Author | Age |
* | Print [Variant] types with the keyword [Variant]. | Arnaud Spiwack | 2014-09-04 |
* | Change the way primitive projections are declared to the kernel. | Matthieu Sozeau | 2014-08-28 |
* | instanciation is French, instantiation is English | Jason Gross | 2014-08-25 |
* | A tentative uniform naming policy in module Inductiveops. | Hugo Herbelin | 2014-08-01 |
* | Reuse universe level substitutions for template polymorphism, fixing performance | Matthieu Sozeau | 2014-05-09 |
* | Fix extraction taking a type in the wrong environment. | Matthieu Sozeau | 2014-05-06 |
* | Fix a pervasive equality use. | Matthieu Sozeau | 2014-05-06 |
* | - Rename eq to equal in Univ, document new modules, set interfaces. | Matthieu Sozeau | 2014-05-06 |
* | Initial work on reintroducing old-style polymorphism for compatibility (the s... | Matthieu Sozeau | 2014-05-06 |
* | This commit adds full universe polymorphism and fast projections to Coq. | Matthieu Sozeau | 2014-05-06 |
* | Fixing Pervasives.equality in extraction. | Pierre-Marie Pédrot | 2014-03-03 |
* | Lazyconstr -> Opaqueproof | Enrico Tassi | 2014-02-26 |
* | New compilation mode -vi2vo | Enrico Tassi | 2014-02-26 |
* | More monomorphic List.mem + List.assoc + ... | letouzey | 2013-10-24 |
* | Removing a bunch of generic equalities. | ppedrot | 2013-09-27 |
* | Declarations.mli: reorganization of modular structures | letouzey | 2013-08-20 |
* | State Transaction Machine | gareuselesinge | 2013-08-08 |
* | Use the Hook module here and there. | ppedrot | 2013-05-12 |
* | Splitting Term into five unrelated interfaces: | ppedrot | 2013-04-29 |
* | Restrict (try...with...) to avoid catching critical exn (part 9) | letouzey | 2013-03-13 |
* | Restrict (try...with...) to avoid catching critical exn (part 6) | letouzey | 2013-03-13 |
* | kernel/declarations becomes a pure mli | letouzey | 2013-02-26 |
* | Names: shortcuts for building {kn, constant, mind} with empty sections | letouzey | 2013-02-26 |
* | Extraction: same as commit 16203, hopefully without NotASort exns | letouzey | 2013-02-18 |
* | Fix extraction of inductive types that Coq auto-detects to be in Prop | letouzey | 2013-02-14 |
* | Modulification of Label | ppedrot | 2012-12-18 |
* | Extraction of projections: restrict a hack to ocaml only (fix #2941) | letouzey | 2012-12-17 |
* | Modulification of identifier | ppedrot | 2012-12-14 |
* | Moved Intset and Intmap to Int namespace. | ppedrot | 2012-12-14 |
* | Extraction Implicit: consider the parameters of a constructor (fix #2905) | letouzey | 2012-10-30 |
* | Cleaning interface of Util. | ppedrot | 2012-09-18 |
* | As r15801: putting everything from Util.array_* to CArray.*. | ppedrot | 2012-09-14 |
* | Moving Utils.list_* to a proper CList module, which includes stdlib | ppedrot | 2012-09-14 |
* | This patch removes unused "open" (automatically generated from | regisgia | 2012-09-14 |
* | The new ocaml compiler (4.00) has a lot of very cool warnings, | regisgia | 2012-09-14 |
* | Fix Extraction Implicit on axioms. | aspiwack | 2012-08-24 |
* | Updating headers. | herbelin | 2012-08-08 |
* | global_reference migrated from Libnames to new Globnames, less deps in gramma... | letouzey | 2012-05-29 |
* | Noise for nothing | pboutill | 2012-03-02 |
* | Extraction: only do the test on generalizable lets for ocaml | letouzey | 2011-12-10 |
* | Extraction: avoid internal eta-reduction (fix #2570) | letouzey | 2011-12-08 |
* | Extraction: try to avoid issues with an Include directly inside a .v | letouzey | 2011-11-30 |
* | Extraction: Richer patterns in matchs as proposed by P.N. Tollitte | letouzey | 2011-11-28 |
* | Extraction Implicit: fix the numbering of constructor arguments | letouzey | 2011-09-05 |
* | Extraction: allow extraction of records with anonymous fields (fix #2555) | letouzey | 2011-08-25 |
* | Extraction: replace generic = on mutual_inductive_body by mib_equal | puech | 2011-07-29 |
* | Set Extraction KeepSingleton: an option for not decapsulating singleton types | letouzey | 2011-07-04 |
* | Extraction: forbid Prop-polymorphism of inductives when extracting to Ocaml | letouzey | 2011-07-04 |
* | Extraction: opaque terms are not traversed anymore by default | letouzey | 2011-04-13 |
* | Lazy loading of opaque proofs: fast as -dont-load-proofs without its drawbacks | letouzey | 2011-04-03 |