| Age | Commit message (Expand) | Author |
|---|
| 2020-11-16 | Explicitly annotate all hint declarations of the standard library. | Pierre-Marie Pédrot |
| 2020-03-19 | [stdlib] Remove a few `auto with *` | Vincent Laporte |
| 2020-03-18 | Update headers in the whole code base. | Théo Zimmermann |
| 2019-10-04 | [Stdlib] OrderedType: do not pollute the “core” hint database | Vincent Laporte |
| 2019-06-17 | Update ml-style headers to new year. | Théo Zimmermann |
| 2019-05-25 | Modifying theories to preferably use the "[= ]" syntax, and, | Hugo Herbelin |
| 2019-04-02 | Remove -compat 8.7 | Jason Gross |
| 2018-11-14 | Deprecate hint declaration/removal with no specified database | Maxime Dénès |
| 2018-10-02 | Update compat notations to be compat 8.7 | Jason Gross |
| 2018-03-05 | Merge PR #6855: Update headers following #6543. | Maxime Dénès |
| 2018-03-02 | Turn warning for deprecated notations on. | Théo Zimmermann |
| 2018-03-02 | Remove the deprecation for some 8.2-8.5 compatibility aliases. | Théo Zimmermann |
| 2018-02-27 | Update headers following #6543. | Théo Zimmermann |
| 2016-07-07 | Merge branch 'v8.5' into v8.6 | Pierre-Marie Pédrot |
| 2016-07-05 | Move option_map notation up | Jason Gross |
| 2016-07-05 | Restore option_map in FMapFacts | Jason Gross |
| 2016-06-18 | Giving a more natural semantics to injection by default. | Hugo Herbelin |
| 2015-12-07 | Fix some typos. | Guillaume Melquiond |
| 2014-07-31 | Adding a generalized version of fold_Equal to FMapFacts. | Pierre Courtieu |
| 2014-06-01 | Making those proofs which depend on names generated for the arguments | Hugo Herbelin |
| 2014-05-06 | This commit adds full universe polymorphism and fast projections to Coq. | Matthieu Sozeau |
| 2014-05-02 | Eta contractions to please cbn | Pierre Boutillier |
| 2012-05-15 | Intuition: temporary(?) restore the unconditional unfolding of not | letouzey |
| 2012-04-15 | Fixing tauto "special" behavior on singleton types w/ 2 parameters (bug #2680). | herbelin |
| 2012-01-31 | Revert "Tentative to fix bug #2628 by not letting intuition break records. Mi... | msozeau |
| 2012-01-28 | Tentative to fix bug #2628 by not letting intuition break records. Might be t... | msozeau |
| 2011-11-21 | theories/, plugins/ and test-suite/ ported to the Arguments vernacular | gareuselesinge |
| 2011-10-14 | MSet/FSet/FMap : add more explicitly an alternative spec for fold via fold_right | letouzey |
| 2011-02-16 | Fix compilation issues. | msozeau |
| 2011-02-14 | - Fix treatment of globality flag for typeclass instance hints (they | msozeau |
| 2010-12-17 | Cosmetic : let's take advantage of the n-ary exists notation | letouzey |
| 2010-10-22 | FMapFacts: typo noticed by Aaron | letouzey |
| 2010-04-29 | Remove the svn-specific $Id$ annotations | letouzey |
| 2009-11-02 | List + SetoidList : some cleanup around predicates Exists, Forall, Forall2, F... | letouzey |
| 2009-10-19 | Merge SetoidList2 into SetoidList. | letouzey |
| 2009-10-08 | Init/Tactics.v: tactic with nicer name 'exfalso' for 'elimtype False' | letouzey |
| 2009-10-08 | Implicit argument of Logic.eq become maximally inserted | letouzey |
| 2009-09-17 | Delete trailing whitespaces in all *.{v,ml*} files | glondu |
| 2009-09-08 | Fix the bug-ridden code used to choose leibniz or generalized | msozeau |
| 2009-07-14 | Simplify eauto and fix it for compatibility, allowing full delta during | msozeau |
| 2009-07-09 | Use the proper unification flags in e_exact. This makes exact fail a bit | msozeau |
| 2009-04-21 | Rename [Morphism] into [Proper] and [respect] into [proper] to comply | msozeau |
| 2009-04-18 | Just export RelationClasses for [Equivalence] through Setoid. | msozeau |
| 2008-12-26 | FMaps: various updates (mostly suggested by P. Casteran) | letouzey |
| 2008-12-22 | FMap: fold_rec + more permissive transpose hyp + various cleanup | letouzey |
| 2008-12-17 | FSet/OrderedType now includes an eq_dec, and hence become an extension of Dec... | letouzey |
| 2008-09-14 | Add user syntax for creating hint databases [Create HintDb foo | msozeau |
| 2008-09-04 | Correction du bug #1937 | notin |
| 2008-06-27 | Enhanced discrimination nets implementation, which can now work with | msozeau |
| 2008-04-12 | Add the ability to specify what to do with free variables in instance | msozeau |
