| Age | Commit message (Expand) | Author |
|---|
| 2020-11-16 | Explicitly annotate all hint declarations of the standard library. | Pierre-Marie Pédrot |
| 2020-05-01 | Fixing #11903: Fixpoints not truly recursive in standard library. | Hugo Herbelin |
| 2020-04-03 | Avoiding using a fixed introduction name in Ltac code of stdlib. | Hugo Herbelin |
| 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-22 | FSets: do not use “omega” | Vincent Laporte |
| 2019-10-04 | [Stdlib] OrderedType: do not pollute the “core” hint database | Vincent Laporte |
| 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 |
| 2019-03-30 | Error when [foo.(bar)] is used with nonprojection [bar] | Gaëtan Gilbert |
| 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 |
| 2014-10-01 | Simpl less (so that cbn will not simpl too much) | Pierre Boutillier |
| 2014-08-25 | instanciation is French, instantiation is English | Jason Gross |
| 2014-08-25 | Grammar: "allowing to" is not proper English | Jason Gross |
| 2014-06-26 | Avoid using a deprecated lemma in the standard library. | Guillaume Melquiond |
| 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 |
| 2013-01-18 | Unset Asymmetric Patterns | pboutill |
| 2012-12-18 | No more constant named "int" in Coq theories (cf bug #2878) | letouzey |
| 2012-10-01 | Ltac repeat is in fact already doing progress | letouzey |
| 2012-07-05 | Kills the useless tactic annotations "in |- *" | letouzey |
| 2012-07-05 | Open Local Scope ---> Local Open Scope, same with Notation and alii | letouzey |
| 2011-05-05 | Modularization of BinInt, related fixes in the stdlib | 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-06-08 | Made option "Automatic Introduction" active by default before too many | herbelin |
| 2010-04-29 | Remove the svn-specific $Id$ annotations | letouzey |
| 2009-10-19 | Merge SetoidList2 into SetoidList. | letouzey |
| 2009-10-16 | Structure/OrderTac.v : highlight the "order" tactic by isolating it from FSet... | letouzey |
| 2009-09-28 | Fix the stdlib doc compilation + switch all .v file to utf8 | letouzey |
| 2009-09-17 | Delete trailing whitespaces in all *.{v,ml*} files | glondu |
| 2009-06-22 | made several occurrences of (eapply ...; eauto) not rely on the lack of patte... | barras |
| 2008-06-01 | Intropattern: syntax {x,y,z,t} becomes (x & y & z & t), as decided in | letouzey |
| 2008-04-17 | Prevent the apparition of &&& when printing a (if ... then ... else false) | letouzey |
| 2008-04-03 | New file FMapFullAVL containing the balancing proofs about FMapAVL: | letouzey |
| 2008-04-03 | Rework of FMapAVL inspired by recent changes of FSetAVL: | letouzey |
| 2008-03-15 | Reorganisation of FSetAVL (consequences of remarks by B. Gregoire) | letouzey |
| 2008-03-07 | repair FSets/FMap after the change in setoid rewrite | letouzey |
| 2008-03-04 | migration from Set to Type of FSet/FMap + some dependencies... | letouzey |
| 2008-02-28 | Some suggestions about FMap by P. Casteran: | letouzey |
| 2008-02-28 | cardinal is promoted to the rank of primitive member of the FMap interface | letouzey |
| 2008-02-10 | Major revision: use of Function, including some non-structural ones | letouzey |
| 2008-02-05 | kill some useless module aliases E:=X (for better name printing, see Elie's 1... | letouzey |
| 2007-11-06 | small tactics "swap" and "absurd_hyp" are now obsolete: "contradict" is | letouzey |
