| Age | Commit message (Expand) | Author |
|---|
| 2017-07-19 | [general] Move files to directories matching linking order. | Emilio Jesus Gallego Arias |
| 2017-07-04 | Bump year in headers. | Pierre-Marie Pédrot |
| 2016-09-30 | Merge remote-tracking branch 'github/pr/299' into v8.6 | Maxime Dénès |
| 2016-09-29 | Fix bug #5036 autorewrite, sections and universes | Matthieu Sozeau |
| 2016-09-29 | Fix bug #4869, allow Prop, Set, and level names in constraints. | Matthieu Sozeau |
| 2016-07-29 | COMMENT: moving misplaced comment where it belongs | Matej Kosik |
| 2016-06-18 | Moving the typing_flags to the environment. | Pierre-Marie Pédrot |
| 2016-06-16 | Factorizing the uses of Declareops.safe_flags. | Pierre-Marie Pédrot |
| 2016-06-16 | Merge PR #79: Let the kernel assume that a (co-)inductive type is positive. | Pierre-Marie Pédrot |
| 2016-06-14 | Assume totality: dedicated type rather than bool | Arnaud Spiwack |
| 2016-01-20 | Update copyright headers. | Maxime Dénès |
| 2016-01-15 | Hooks for a third-party XML plugin. Contributed by Claudio Sacerdoti Coen. | Maxime Dénès |
| 2015-10-30 | Add a way to get the right fix_exn in external vernacular commands | Matthieu Sozeau |
| 2015-10-28 | Avoid type checking private_constants (side_eff) again during Qed (#4357). | Enrico Tassi |
| 2015-10-27 | Fix bugs 4389, 4390 and 4391 due to wrong handling of universe names | Matthieu Sozeau |
| 2015-09-25 | Propagate `Guarded` flag from syntax to kernel. | Arnaud Spiwack |
| 2015-09-23 | Hopefully better names to constructors of internal_flag, as discussed | Hugo Herbelin |
| 2015-02-14 | Abstract: "Qed export ident, .., ident" to preserve v8.4 behavior | Enrico Tassi |
| 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-09-08 | Removing dead code relative to the XML plugin. | Pierre-Marie Pédrot |
| 2014-07-01 | Add toplevel commands to declare global universes and constraints. | Matthieu Sozeau |
| 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 |
| 2014-03-05 | Remove many superfluous 'open' indicated by ocamlc -w +33 | Pierre Letouzey |
| 2013-08-30 | ind_tables: properly handling side effects | gareuselesinge |
| 2013-05-12 | Use the Hook module here and there. | ppedrot |
| 2013-05-09 | Use definition_entry to declare local definitions | gareuselesinge |
| 2013-04-29 | Merging Context and Sign. | ppedrot |
| 2013-03-11 | Added a Local Definition vernacular command. This type of definition | ppedrot |
| 2013-02-19 | Dir_path --> DirPath | letouzey |
| 2012-12-14 | Modulification of dir_path | ppedrot |
| 2012-12-14 | Modulification of identifier | ppedrot |
| 2012-10-26 | Change Hint Resolve, Immediate to take a global reference as argument | msozeau |
| 2012-08-08 | Updating headers. | herbelin |
| 2011-10-08 | Rely on kernel to know if a name is already used so as to be consistent with it. | herbelin |
| 2010-09-02 | * removed declare_constant and declare_internal_constant | vsiles |
| 2010-07-24 | Updated all headers for 8.3 and trunk | herbelin |
| 2010-06-29 | change the flag "internal" in declare/ind_tables from bool to | vsiles |
| 2010-06-22 | New script dev/tools/change-header to automatically update Coq files headers. | herbelin |
| 2010-04-29 | Remove the svn-specific $Id$ annotations | letouzey |
| 2010-04-29 | Move from ocamlweb to ocamdoc to generate mli documentation | pboutill |
| 2009-11-08 | Restructuration of command.ml + generic infrastructure for inductive schemes | herbelin |
| 2009-09-17 | Delete trailing whitespaces in all *.{v,ml*} files | glondu |
| 2009-09-14 | Backtrack on the forced discharge of type class variables introduced | msozeau |
| 2009-08-06 | - Cleaning phase of the interfaces of libnames.ml and nametab.ml | herbelin |
| 2009-05-27 | Fix implicit args code so that declarations are added for all | msozeau |
| 2009-01-17 | DISCLAIMER | puech |
| 2008-04-23 | Prise en compte des coercions dans les clauses "with" même si le type | herbelin |
| 2008-04-02 | Add the ability to specify the implicit status of section variables and | msozeau |
