| Age | Commit message (Expand) | Author |
|---|
| 2021-03-26 | remove in List.v deprecated/unnecessary dependencies: Le, Gt, Minus, Lt, Setoid | Andrej Dudenhefner |
| 2021-01-18 | Support locality attributes for Hint Rewrite (including export) | Gaëtan Gilbert |
| 2020-11-16 | Explicitly annotate all hint declarations of the standard library. | Pierre-Marie Pédrot |
| 2020-03-19 | firstorder: default tactic is “auto with core” | Vincent Laporte |
| 2020-03-18 | Update headers in the whole code base. | Théo Zimmermann |
| 2019-12-17 | [micromega] fix efficiency regression | Frédéric Besson |
| 2019-11-25 | MSets: use “lia” rather than “omega” | Vincent Laporte |
| 2019-09-03 | New lemmas for List.v | Oliver Nash |
| 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-05-25 | Modifying theories to preferably use the "[= ]" syntax, and, | Hugo Herbelin |
| 2019-05-23 | Fixing typos - Part 3 | JPR |
| 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-08-22 | Fix typo of caracterisation -> c*h*aracterisation | Siddharth Bhat |
| 2018-08-18 | Merge PR #8272: Fix typo in documentation, heigth --> height. | Théo Zimmermann |
| 2018-08-17 | Fix typo in documentation, heigth --> height. | Nick Lewycky |
| 2018-02-27 | Update headers following #6543. | Théo Zimmermann |
| 2017-08-21 | Ensuring all .v files end with a newline to make "sed -i" work better on them. | Hugo Herbelin |
| 2017-06-14 | Prelude : no more autoload of plugins extraction and recdef | Pierre Letouzey |
| 2017-06-01 | drop vo.itarget files and compute the corresponding the corresponding values ... | Matej Kosik |
| 2016-11-24 | Fix some documentation typos. | Guillaume Melquiond |
| 2016-10-12 | Merge branch 'v8.5' into v8.6 | Pierre-Marie Pédrot |
| 2016-10-03 | Remove if_then_else. Use tryif instead. | Théo Zimmermann |
| 2016-06-18 | Giving a more natural semantics to injection by default. | Hugo Herbelin |
| 2016-06-16 | Typeclasses: stdlib fixes for new search algorithm | Matthieu Sozeau |
| 2016-06-03 | Removing "intro" from the tactic AST. | Pierre-Marie Pédrot |
| 2016-04-27 | Revert "Temporary hack to compensate missing comma while re-printing tactic" | Hugo Herbelin |
| 2016-04-27 | Temporary hack to compensate missing comma while re-printing tactic | Hugo Herbelin |
| 2015-04-02 | ZArith/Int.v: some modernizations | Pierre Letouzey |
| 2015-03-06 | MMapPositive: another implementation of MMaps | Pierre Letouzey |
| 2014-12-25 | Forbid Require inside interactive modules and module types. | Maxime Dénès |
| 2014-10-01 | Simpl less (so that cbn will not simpl too much) | Pierre Boutillier |
| 2014-09-27 | Keyed unification option, compiling the whole standard library | Matthieu Sozeau |
| 2014-08-25 | "allows to", like "allowing to", is improper | Jason Gross |
| 2014-07-10 | MSetRBT: unfortunate typo in compare_height (fix #3413) | Pierre Letouzey |
| 2014-07-09 | Arith: full integration of the "Numbers" modular framework | Pierre Letouzey |
| 2014-06-26 | Avoid using a deprecated lemma in the standard library. | Guillaume Melquiond |
| 2014-06-04 | Make standard library independent of the names generated by | Hugo Herbelin |
| 2014-06-01 | Making those proofs which depend on names generated for the arguments | Hugo Herbelin |
| 2014-05-09 | Restore implicit arguments of irreflexivity (fixes bug #3305). | Matthieu Sozeau |
| 2014-05-06 | Try a new way of handling template universe levels | Matthieu Sozeau |
| 2014-05-06 | - Fix arity handling in retyping (de Bruijn bug!) | Matthieu Sozeau |
| 2014-05-06 | - Fix bug preventing apply from unfolding Fixpoints. | Matthieu Sozeau |
| 2014-05-06 | Correct rebase on STM code. Thanks to E. Tassi for help on dealing with | Matthieu Sozeau |
| 2014-05-06 | This commit adds full universe polymorphism and fast projections to Coq. | Matthieu Sozeau |
| 2014-05-02 | Cbn is happier when ?SetPositive fixpoints have the set as recursive argument | Pierre Boutillier |
| 2014-05-02 | Eta contractions to please cbn | Pierre Boutillier |
