| Age | Commit message (Expand) | Author |
|---|
| 2016-09-29 | Extraction: ignore some useless stuff about universes | Pierre Letouzey |
| 2016-07-03 | errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod... | Pierre Letouzey |
| 2016-07-01 | Separate flags for fix/cofix/match reduction and clean reduction function names. | Maxime Dénès |
| 2016-06-27 | Merge branch 'v8.5' | Pierre-Marie Pédrot |
| 2016-06-23 | Fix typo. | Guillaume Melquiond |
| 2016-06-01 | Merge branch 'v8.5' | Pierre-Marie Pédrot |
| 2016-05-30 | Extraction : add a location in the error message about polyprop | Pierre Letouzey |
| 2016-05-30 | Extraction : add a location in the error message about polyprop | Pierre Letouzey |
| 2016-05-23 | Extraction/Projections: Fix bug #4710 | Matthieu Sozeau |
| 2016-05-04 | Merge branch 'v8.5' | Pierre-Marie Pédrot |
| 2016-05-04 | Handle primitive projections inside types when extracting (bug #4616). | Guillaume Melquiond |
| 2016-02-09 | CLEANUP: Context.{Rel,Named}.Declaration.t | Matej Kosik |
| 2016-01-21 | Merge branch 'v8.5' | Pierre-Marie Pédrot |
| 2016-01-20 | Update copyright headers. | Maxime Dénès |
| 2016-01-11 | CLEANUP: kernel/context.ml{,i} | Matej Kosik |
| 2015-12-15 | Extraction: more cautious use of intermediate result caching (fix #3923) | Pierre Letouzey |
| 2015-12-12 | Extraction: nicer implementation of Implicits | Pierre Letouzey |
| 2015-12-07 | Fix some typos. | Guillaume Melquiond |
| 2015-07-22 | Extraction: fix primitive projection extraction. | Matthieu Sozeau |
| 2015-01-12 | Update headers. | Maxime Dénès |
| 2015-01-11 | Extraction: no more ascii blob in type variables (fix #3227) | Pierre Letouzey |
| 2015-01-11 | Extraction : some more support functions for a future "Extraction Compute" | Pierre Letouzey |
| 2015-01-11 | Extraction: minor tweaks to ease ongoing experiments about Lambda | Pierre Letouzey |
| 2014-10-13 | library/opaqueTables: enable their use in interactive mode | Enrico Tassi |
| 2014-10-11 | Revert d0cd27e209be08ee51a2d609157367f053438a10: giving a different name | Matthieu Sozeau |
| 2014-09-27 | Add a boolean to indicate the unfolding state of a primitive projection, | Matthieu Sozeau |
| 2014-09-04 | Print [Variant] types with the keyword [Variant]. | Arnaud Spiwack |
| 2014-08-28 | Change the way primitive projections are declared to the kernel. | Matthieu Sozeau |
| 2014-08-25 | instanciation is French, instantiation is English | Jason Gross |
| 2014-08-01 | A tentative uniform naming policy in module Inductiveops. | Hugo Herbelin |
| 2014-05-09 | Reuse universe level substitutions for template polymorphism, fixing performance | Matthieu Sozeau |
| 2014-05-06 | 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-03-03 | Fixing Pervasives.equality in extraction. | Pierre-Marie Pédrot |
| 2014-02-26 | Lazyconstr -> Opaqueproof | Enrico Tassi |
| 2014-02-26 | New compilation mode -vi2vo | Enrico Tassi |
| 2013-10-24 | More monomorphic List.mem + List.assoc + ... | letouzey |
| 2013-09-27 | Removing a bunch of generic equalities. | ppedrot |
| 2013-08-20 | Declarations.mli: reorganization of modular structures | letouzey |
| 2013-08-08 | State Transaction Machine | gareuselesinge |
| 2013-05-12 | Use the Hook module here and there. | ppedrot |
| 2013-04-29 | Splitting Term into five unrelated interfaces: | ppedrot |
| 2013-03-13 | 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-02-26 | kernel/declarations becomes a pure mli | letouzey |
| 2013-02-26 | Names: shortcuts for building {kn, constant, mind} with empty sections | letouzey |
| 2013-02-18 | Extraction: same as commit 16203, hopefully without NotASort exns | letouzey |
