| Age | Commit message (Expand) | Author |
|---|
| 2019-05-25 | Modifying theories to preferably use the "[= ]" syntax, and, | Hugo Herbelin |
| 2019-05-23 | Fixing typos - Part 3 | JPR |
| 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-04-13 | [ltac] Deprecate nameless fix/cofix. | Emilio Jesus Gallego Arias |
| 2018-03-07 | [stdlib] Do not use “Require” inside sections | Vincent Laporte |
| 2018-02-27 | Update headers following #6543. | Théo Zimmermann |
| 2017-07-04 | Bump year in headers. | Pierre-Marie Pédrot |
| 2017-06-01 | drop vo.itarget files and compute the corresponding the corresponding values ... | Matej Kosik |
| 2016-06-18 | Giving a more natural semantics to injection by default. | Hugo Herbelin |
| 2016-01-21 | Merge branch 'v8.5' | Pierre-Marie Pédrot |
| 2016-01-21 | Stronger invariants on the use of the introduction pattern (pat1,...,patn). | Hugo Herbelin |
| 2016-01-20 | Update copyright headers. | Maxime Dénès |
| 2015-07-31 | Remove some outdated files and fix permissions. | Guillaume Melquiond |
| 2015-01-12 | Update headers. | Maxime Dénès |
| 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-12 | Now parsing rules of ML-declared tactics are only made available after the | Pierre-Marie Pédrot |
| 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-02-07 | FinFun.v: results about injective/surjective/bijective fonctions over finite ... | Pierre Letouzey |
| 2013-06-02 | Making the behavior of "injection ... as ..." more natural: | herbelin |
| 2012-08-08 | Updating headers. | herbelin |
| 2012-07-10 | isolate instances about Permutation and PermutationA which may slow rewrite | letouzey |
| 2012-07-09 | induction/destruct : nicer syntax for generating equations (solves #2741) | letouzey |
| 2012-07-05 | Kills the useless tactic annotations "in |- *" | letouzey |
| 2012-07-05 | ZArith + other : favor the use of modern names instead of compat notations | letouzey |
| 2012-05-22 | Permutation: remove a compatibility notation which doesn't help MathClasses | letouzey |
| 2012-05-18 | List + Permutation : more results about nth_error and nth | letouzey |
| 2011-11-21 | theories/, plugins/ and test-suite/ ported to the Arguments vernacular | gareuselesinge |
| 2011-09-16 | Omega: for non-arithmetical goals, try proving False from context (wish #2236) | letouzey |
| 2011-03-04 | Simplify proofs in Permutation using generalized rewriting. | msozeau |
| 2011-02-10 | Remove obsolete TheoryList | glondu |
| 2010-12-09 | In passing, very quick uniformization of coqdoc headers in a few files. | herbelin |
| 2010-12-04 | Fixing coqdoc pretty-printing of a table in Mergesort. Incidentally, | herbelin |
| 2010-07-28 | Rewrite Heap merging so that it extracts to an O(n log n) definition. | msozeau |
| 2010-07-24 | Updated all headers for 8.3 and trunk | herbelin |
| 2010-07-02 | Sorting library: export as hints only lemmas that obviously simplify | herbelin |
| 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-02-16 | Uniformisation Sorting/Mergesort and Structures/Orders | letouzey |
| 2010-01-30 | Update CHANGES, add documentation for new commands/tactics and do a bit | msozeau |
| 2009-12-13 | Addition of mergesort + cleaning of the Sorting library | herbelin |
| 2009-12-09 | Factorisation between Makefile and ocamlbuild systems : .vo to compile are in... | letouzey |
| 2009-11-02 | Sorting/Permutation: no need to require the whole Arith (and hence plugins li... | letouzey |
| 2009-10-19 | Merge SetoidList2 into SetoidList. | letouzey |
| 2009-09-17 | Delete trailing whitespaces in all *.{v,ml*} files | glondu |
| 2009-08-04 | - Add more precise error localisation when one of the application fails | herbelin |
