| Age | Commit message (Expand) | Author |
|---|
| 2019-08-19 | [api] Move handling of variable implicit data to impargs | Emilio Jesus Gallego Arias |
| 2019-07-01 | [api] Reduce declare_kinds even more. | Emilio Jesus Gallego Arias |
| 2019-07-01 | [api] Refactor most of `Decl_kinds` | Emilio Jesus Gallego Arias |
| 2019-06-24 | [api] [proof] Move `discharge` type to vernac_ast where it is used. | Emilio Jesus Gallego Arias |
| 2019-06-24 | [api] Remove `polymorphic` type alias, use labels instead. | Emilio Jesus Gallego Arias |
| 2019-06-24 | [api] Move `locality` from `library` to `vernac`. | Emilio Jesus Gallego Arias |
| 2019-06-24 | [lemmas] [proof] Split proof kinds into per-layer components. | Emilio Jesus Gallego Arias |
| 2019-06-24 | [proof] Remove duplicated universe polymorphic from decl_kinds | Emilio Jesus Gallego Arias |
| 2019-06-17 | Update ml-style headers to new year. | Théo Zimmermann |
| 2019-06-08 | Cleaning the status of Local Definition and similar. | Hugo Herbelin |
| 2019-06-08 | Adding a new kind of assumption to track assumption coming from "Context". | Hugo Herbelin |
| 2019-02-04 | Primitive integers | Maxime Dénès |
| 2018-12-14 | [proof] Rework proof interface. | Emilio Jesus Gallego Arias |
| 2018-05-30 | [api] Remove deprecated object from `Term` | Emilio Jesus Gallego Arias |
| 2018-04-23 | [api] Relocate `intf` modules according to dependency-order. | Emilio Jesus Gallego Arias |
| 2012-05-29 | Decl_kinds becomes a pure mli file, remaining ops in new file kindops.ml | letouzey |
| 2012-03-02 | Noise for nothing | pboutill |
| 2011-04-13 | Revert "Add [Polymorphic] flag for defs" | msozeau |
| 2011-04-13 | Add [Polymorphic] flag for defs | msozeau |
| 2011-01-28 | Remove the "Boxed" syntaxes and the const_entry_boxed field | letouzey |
| 2010-07-24 | Updated all headers for 8.3 and trunk | herbelin |
| 2010-04-29 | Remove the svn-specific $Id$ annotations | letouzey |
| 2009-09-17 | Delete trailing whitespaces in all *.{v,ml*} files | glondu |
| 2009-01-19 | Les records déclarés avec Record ne peuvent plus être récursifs (le | aspiwack |
| 2008-05-30 | Improvements on coqdoc by adding more information into .glob | msozeau |
| 2008-04-23 | Prise en compte des coercions dans les clauses "with" même si le type | herbelin |
| 2007-12-31 | Merged revisions 10358-10362,10365,10371-10373,10377,10383-10384,10394-10395,... | msozeau |
| 2006-01-29 | Ajout syntaxe concrète Proposition, synonyme de Lemma | herbelin |
| 2006-01-28 | - Ajout syntaxe concrète Property/Corollary, synonymes de Lemma | herbelin |
| 2004-10-20 | COMMITED BYTECODE COMPILER | barras |
| 2004-10-11 | Suppression IsConjecture redondant avec Conjectural | herbelin |
| 2004-07-16 | Nouvelle en-tête | herbelin |
| 2003-10-23 | Conjecture declare maintenant un axiome; reorganisation VernacDefinition | herbelin |
| 2003-10-08 | Mise en place d'un couple 'Conjecture/Admitted' pour déclarer un énoncé in... | herbelin |
| 2003-03-13 | Ajout réaffichage SubClass | herbelin |
| 2003-02-05 | Ajout du traducteur | desmettr |
| 2002-11-05 | Intégration des modifs de la branche mowgli : | herbelin |
