| Age | Commit message (Expand) | Author |
|---|
| 2015-07-10 | Option -type-in-type: added support in checker and making it contaminating | Hugo Herbelin |
| 2015-06-24 | Add corresponding field in `VernacInductive`. | Arnaud Spiwack |
| 2015-06-24 | Add a corresponding field in `mutual_inductive_entry` (part 1). | Arnaud Spiwack |
| 2015-03-08 | Fixing bug #2951. | Pierre-Marie Pédrot |
| 2015-01-17 | Make native compiler handle universe polymorphic definitions. | Maxime Dénès |
| 2015-01-12 | Update headers. | Maxime Dénès |
| 2015-01-05 | kernel/ind Change interface of declare_mind and declare_mutual | Matthieu Sozeau |
| 2014-11-23 | Pass around information on the use of template polymorphism for | Matthieu Sozeau |
| 2014-10-25 | This commit introduces changes in induction and destruct. | Hugo Herbelin |
| 2014-10-11 | Revert d0cd27e209be08ee51a2d609157367f053438a10: giving a different name | Matthieu Sozeau |
| 2014-10-10 | Give the same argument name for the record binder of type class | Matthieu Sozeau |
| 2014-09-30 | Add syntax for naming new goals in refine: writing ?[id] instead of _ | Hugo Herbelin |
| 2014-09-27 | Add a boolean to indicate the unfolding state of a primitive projection, | Matthieu Sozeau |
| 2014-09-15 | Rework typeclass resolution and control of backtracking. | Matthieu Sozeau |
| 2014-09-13 | Providing a -type-in-type option for collapsing the universe hierarchy. | Hugo Herbelin |
| 2014-09-12 | Uniformisation of the order of arguments env and sigma. | Hugo Herbelin |
| 2014-09-11 | Add a flag for restricting resolution of typeclasses to | Matthieu Sozeau |
| 2014-09-04 | Remove [Infer] option of records. | Arnaud Spiwack |
| 2014-09-04 | Types declared as Variants really do not accept recursive definitions. | Arnaud Spiwack |
| 2014-09-04 | Print [Variant] types with the keyword [Variant]. | Arnaud Spiwack |
| 2014-08-30 | Simplify even further the declaration of primitive projections, | Matthieu Sozeau |
| 2014-08-29 | Fix bug when defining primitive projections mixing defined and abstracts fields. | Matthieu Sozeau |
| 2014-08-28 | Change the way primitive projections are declared to the kernel. | Matthieu Sozeau |
| 2014-08-03 | Move to a representation of universe polymorphic constants using indices for ... | Matthieu Sozeau |
| 2014-07-25 | - Do module substitution inside mind_record. | Matthieu Sozeau |
| 2014-06-20 | Cleanup treatment of template universe polymorphism (thanks to E. Tassi | Matthieu Sozeau |
| 2014-06-18 | Proofs now take and return an evar_universe_context, simplifying interfaces | Matthieu Sozeau |
| 2014-06-17 | Complying an ocaml warning. | Hugo Herbelin |
| 2014-06-17 | Safer entry point of primitive projections in the kernel, now it does recognize | Matthieu Sozeau |
| 2014-05-06 | Allow records whose sort is defined by a constant. | Matthieu Sozeau |
| 2014-05-06 | - Fix bug preventing apply from unfolding Fixpoints. | Matthieu Sozeau |
| 2014-05-06 | Adapt universe polymorphic branch to new handling of futures for delayed proofs. | Matthieu Sozeau |
| 2014-05-06 | Adapt Y. Bertot's path on private inductives (now the keyword is "Private"). | Yves Bertot |
| 2014-05-06 | Rework handling of universes on top of the STM, allowing for delayed | Matthieu Sozeau |
| 2014-05-06 | This commit adds full universe polymorphism and fast projections to Coq. | Matthieu Sozeau |
| 2013-12-24 | Qed: feedback when type checking is done | Enrico Tassi |
| 2013-11-27 | Adding generic solvers to term holes. For now, no resolution mechanism nor | Pierre-Marie Pédrot |
| 2013-10-23 | cList: a few alternative to hashtbl-based uniquize, distinct, subset | letouzey |
| 2013-09-18 | Removing almost all new_untyped_evar, and a bunch of Evd.add. | ppedrot |
| 2013-09-12 | Unplugging Autoinstance. The code is still here if someone wishes | ppedrot |
| 2013-08-08 | State Transaction Machine | gareuselesinge |
| 2013-05-09 | A uniformization step around understand_* and interp_* functions. | herbelin |
| 2013-04-29 | Splitting Term into five unrelated interfaces: | ppedrot |
| 2013-03-11 | Added a Local Definition vernacular command. This type of definition | ppedrot |
| 2013-01-28 | Uniformization of the "anomaly" command. | ppedrot |
| 2013-01-22 | New implementation of the conversion test, using normalization by evaluation to | mdenes |
| 2012-12-18 | Modulification of name | ppedrot |
| 2012-12-14 | Modulification of identifier | ppedrot |
| 2012-11-26 | Monomorphization (toplevel) | ppedrot |
| 2012-11-17 | Taking into account the type of a definition (if it exists), and the | herbelin |
