| Age | Commit message (Expand) | Author |
|---|
| 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-04-23 | Import proof of decidability of negated formulas from Coquelicot. | Guillaume Melquiond |
| 2014-04-22 | Remove some uses of excluded middle. | Guillaume Melquiond |
| 2014-04-22 | Replace the proof of sig_forall_dec from Kaliszyk/O'Connor by the one from Co... | Guillaume Melquiond |
| 2014-04-16 | Fixing missing headers. | Hugo Herbelin |
| 2014-04-10 | No more Coersion in Init. | Pierre Boutillier |
| 2014-03-10 | Add missing lemmas: Rplus_eq_compat_r and Rplus_eq_reg_r. | Guillaume Melquiond |
| 2013-12-04 | Add lemma derivable_pt_lim_atan. | Guillaume Melquiond |
| 2013-12-03 | Fix statement of Rplus_lt_reg_r and add Rplus_lt_reg_l. | Guillaume Melquiond |
| 2013-12-03 | Remove a useless hypothesis from Rle_Rinv. | Guillaume Melquiond |
| 2013-01-18 | Unset Asymmetric Patterns | pboutill |
| 2012-10-26 | Change Hint Resolve, Immediate to take a global reference as argument | msozeau |
| 2012-10-16 | Removing redundant definition of case_eq (see #2919). | herbelin |
| 2012-08-08 | Updating headers. | herbelin |
| 2012-07-05 | Legacy Ring and Legacy Field migrated to contribs | letouzey |
| 2012-07-05 | Some cleanup in recent proofs concerning pi | 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 |
| 2012-07-05 | ZArith + other : favor the use of modern names instead of compat notations | letouzey |
| 2012-06-11 | These files are displaced from Rtrigo.v and Ranalysis_reg.v | bertot |
| 2012-06-11 | finish the rearrangement for removing the sin_PI2 axiom. This new version | bertot |
| 2012-06-11 | Adds the proof of PI_ineq, plus some other smarter ways to approximate PI | bertot |
| 2012-06-05 | Modifications and rearrangements to remove the action that sin (PI/2) = 1 | bertot |
| 2012-04-15 | Fixing tauto "special" behavior on singleton types w/ 2 parameters (bug #2680). | herbelin |
| 2011-11-21 | theories/, plugins/ and test-suite/ ported to the Arguments vernacular | gareuselesinge |
| 2011-11-03 | Cleaning a little bit the files talking about descriptions: avoiding | herbelin |
| 2011-05-05 | BinInt: Z.add become the alternative Z.add' | letouzey |
| 2011-04-13 | - Improve unification (beta-reduction, and same heuristic as evarconv for red... | msozeau |
| 2011-04-13 | Fix scripts relying on unification not doing any beta reduction. | msozeau |
| 2011-04-13 | Unify meta types with the right flags, add betaiotazeta reduction to unificat... | msozeau |
| 2011-03-17 | CompareSpec: a slight generalization/reformulation of CompSpec | letouzey |
| 2011-01-28 | Remove the "Boxed" syntaxes and the const_entry_boxed field | letouzey |
| 2010-12-10 | First release of Vector library. | pboutill |
| 2010-11-18 | Some more revision of {P,N,Z}Arith + bitwise ops in Ndigits | letouzey |
| 2010-10-21 | Solve name conflict about pow introduced by commit 13546. | letouzey |
| 2010-10-14 | Numbers: new functions pow, even, odd + many reorganisations | letouzey |
| 2010-07-24 | Updated all headers for 8.3 and trunk | herbelin |
| 2010-04-29 | Remove the svn-specific $Id$ annotations | letouzey |
| 2010-04-22 | Here comes the commit, announced long ago, of the new tactic engine. | aspiwack |
| 2010-02-18 | Removed redundant and ill-named technical lemma. | gmelquio |
| 2010-02-18 | Removed SeqProp's dependency on Classical. | gmelquio |
| 2010-02-18 | Removed Rtrigo's dependency on Classical. | gmelquio |
| 2010-02-17 | Removed Rseries' dependency on Classical. | gmelquio |
| 2010-02-17 | Removed Rlimit's dependency on Classical. | gmelquio |
| 2010-02-17 | Removed Rderiv's dependency on Classical. | gmelquio |
| 2010-01-07 | Nicer names: DecidableType2* --> Equalities*, OrderedType2* --> Orders* | letouzey |
| 2010-01-07 | Rework of GenericMinMax: new axiomatic, split logical/decidable parts, Leibni... | letouzey |
| 2010-01-07 | OrderTac: use TotalOrder, no more "change" before calling "order" (stuff with... | letouzey |
| 2009-12-17 | Reverse order of arguments in min_case_strong for better uniformity (and comp... | letouzey |
