| Commit message (Expand) | Author | Age |
|---|
| * | More proofs independent of the names generated by induction/elim over |  Hugo Herbelin | 2014-08-05 |
| * | Deactivate the "Standard Propositions Naming" flag, source of a lot of | Hugo Herbelin | 2014-06-26 |
| * | Make standard library independent of the names generated by | Hugo Herbelin | 2014-06-04 |
| * | Make standard library independent of the names generated by | Hugo Herbelin | 2014-06-04 |
| * | Remove spurious Show in script. |  Matthieu Sozeau | 2014-06-04 |
| * | Making those proofs which depend on names generated for the arguments | Hugo Herbelin | 2014-06-01 |
| * | Now parsing rules of ML-declared tactics are only made available after the |  Pierre-Marie Pédrot | 2014-05-12 |
| * | 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-06 |
| * | Import proof of decidability of negated formulas from Coquelicot. |  Guillaume Melquiond | 2014-04-23 |
| * | 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-22 |
| * | Fixing missing headers. | Hugo Herbelin | 2014-04-16 |
| * | No more Coersion in Init. |  Pierre Boutillier | 2014-04-10 |
| * | Add missing lemmas: Rplus_eq_compat_r and Rplus_eq_reg_r. | Guillaume Melquiond | 2014-03-10 |
| * | Add lemma derivable_pt_lim_atan. | Guillaume Melquiond | 2013-12-04 |
| * | 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-12-03 |
| * | Unset Asymmetric Patterns |  pboutill | 2013-01-18 |
| * | Change Hint Resolve, Immediate to take a global reference as argument |  msozeau | 2012-10-26 |
| * | Removing redundant definition of case_eq (see #2919). |  herbelin | 2012-10-16 |
| * | Updating headers. | herbelin | 2012-08-08 |
| * | 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-07-05 |
| * | 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-11 |
| * | Modifications and rearrangements to remove the action that sin (PI/2) = 1 | bertot | 2012-06-05 |
| * | Fixing tauto "special" behavior on singleton types w/ 2 parameters (bug #2680). | herbelin | 2012-04-15 |
| * | theories/, plugins/ and test-suite/ ported to the Arguments vernacular |  gareuselesinge | 2011-11-21 |
| * | Cleaning a little bit the files talking about descriptions: avoiding | herbelin | 2011-11-03 |
| * | BinInt: Z.add become the alternative Z.add' | letouzey | 2011-05-05 |
| * | - 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-04-13 |
| * | CompareSpec: a slight generalization/reformulation of CompSpec | letouzey | 2011-03-17 |
| * | Remove the "Boxed" syntaxes and the const_entry_boxed field | letouzey | 2011-01-28 |
| * | First release of Vector library. | pboutill | 2010-12-10 |
| * | Some more revision of {P,N,Z}Arith + bitwise ops in Ndigits | letouzey | 2010-11-18 |
| * | Solve name conflict about pow introduced by commit 13546. | letouzey | 2010-10-21 |
| * | Numbers: new functions pow, even, odd + many reorganisations | letouzey | 2010-10-14 |
| * | Updated all headers for 8.3 and trunk | herbelin | 2010-07-24 |
| * | Remove the svn-specific $Id$ annotations | letouzey | 2010-04-29 |
| * | Here comes the commit, announced long ago, of the new tactic engine. |  aspiwack | 2010-04-22 |
| * | 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-18 |
Hugo Herbelin
Matthieu Sozeau
Pierre-Marie Pédrot
Guillaume Melquiond
Pierre Boutillier
pboutill
msozeau
herbelin
letouzey
bertot
gareuselesinge
aspiwack
gmelquio