| Age | Commit message (Expand) | Author |
|---|
| 2020-03-18 | Update headers in the whole code base. | Théo Zimmermann |
| 2019-08-26 | Make kernel parametric on the lowest universe and fix #9294 | Matthieu Sozeau |
| 2019-06-17 | Update ml-style headers to new year. | Théo Zimmermann |
| 2018-12-19 | Put #[universes(template)] on all auto template spots in stdlib | Gaëtan Gilbert |
| 2018-11-14 | Deprecate hint declaration/removal with no specified database | Maxime Dénès |
| 2018-09-10 | Adapting standard library to the introduction of "Declare Scope". | Hugo Herbelin |
| 2018-02-27 | Update headers following #6543. | Théo Zimmermann |
| 2017-06-14 | Prelude : no more autoload of plugins extraction and recdef | Pierre Letouzey |
| 2016-06-03 | Removing "intro" from the tactic AST. | Pierre-Marie Pédrot |
| 2015-04-02 | ZArith/Int.v: some modernizations | Pierre Letouzey |
| 2014-08-25 | "allows to", like "allowing to", is improper | Jason Gross |
| 2013-07-17 | "Boolean Equality" and "Case Analysis" are already off by default... | letouzey |
| 2012-12-18 | No more constant named "int" in Coq theories (cf bug #2878) | letouzey |
| 2012-10-26 | Change Hint Resolve, Immediate to take a global reference as argument | msozeau |
| 2012-04-13 | MSetRBT : implementation of MSets via Red-Black trees | letouzey |
| 2012-01-17 | MSetAVL: better implementation of filter suggested by X. Leroy | letouzey |
| 2011-11-21 | theories/, plugins/ and test-suite/ ported to the Arguments vernacular | gareuselesinge |
| 2011-05-05 | Modularization of BinInt, related fixes in the stdlib | letouzey |
| 2011-03-17 | CompareSpec: a slight generalization/reformulation of CompSpec | letouzey |
| 2011-02-17 | - Use transparency information all the way through unification and | msozeau |
| 2011-01-06 | s/appartness/membership/g (Closes: #2470) | glondu |
| 2010-09-20 | Extraction: re-introduce some eta-expansions in rare situations leading to '_... | letouzey |
| 2010-09-17 | For the moment, two small manual eta-expansions to avoid '_a after extraction | letouzey |
| 2010-07-22 | Made notations for exists, exists! and notations of Utf8.v recursive notations | herbelin |
| 2010-06-15 | MSetAVL: for nicer extraction, we create only tree_ind, not tree_rect and tre... | letouzey |
| 2010-06-08 | Made option "Automatic Introduction" active by default before too many | herbelin |
| 2010-04-29 | Remove the svn-specific $Id$ annotations | letouzey |
| 2010-01-12 | MSets: Class Ok becomes a definition instead of an inductive (thanks Matthieu) | letouzey |
| 2010-01-07 | MSetAVL: hints made local since some of them are quite violent (transitivity) | letouzey |
| 2010-01-05 | Avoid declaring hints about refl/sym/trans of eq in DecidableType2 | letouzey |
| 2009-11-15 | Fix [Instance: forall ..., C args := t] declarations to behave as | msozeau |
| 2009-11-08 | Use generalizable variables info when internalizing arbitrary bindings, | msozeau |
| 2009-11-03 | Better visibility of the inductive CompSpec used to specify comparison functions | letouzey |
| 2009-11-03 | OrderedType implementation for various numerical datatypes + min/max structures | letouzey |
| 2009-10-16 | OrderedType2 : trivial lemmas are turned into tests for order. | letouzey |
| 2009-10-13 | MSets: a new generation of FSets | letouzey |
