| Commit message (Expand) | Author | Age |
|---|
| * | "allows to", like "allowing to", is improper |  Jason Gross | 2014-08-25 |
| * | instanciation is French, instantiation is English | Jason Gross | 2014-08-25 |
| * | Move to a representation of universe polymorphic constants using indices for ... |  Matthieu Sozeau | 2014-08-03 |
| * | Arith: full integration of the "Numbers" modular framework |  Pierre Letouzey | 2014-07-09 |
| * | Move Params definition in generalize rewriting out of a section so that | Matthieu Sozeau | 2014-06-29 |
| * | Export the right modules in Setoid, avoiding anomalies in generalized rewriting. | Matthieu Sozeau | 2014-06-26 |
| * | - Fix in kernel conversion not folding the universe constraints |  Matthieu Sozeau | 2014-05-26 |
| * | Update and start testing rewrite-in-type code. | Matthieu Sozeau | 2014-05-09 |
| * | Restore implicit arguments of irreflexivity (fixes bug #3305). | Matthieu Sozeau | 2014-05-09 |
| * | - Fix bug preventing apply from unfolding Fixpoints. | Matthieu Sozeau | 2014-05-06 |
| * | Fix issue #88: restrict_universe_context was wrongly forgetting about constra... | Matthieu Sozeau | 2014-05-06 |
| * | This commit adds full universe polymorphism and fast projections to Coq. | Matthieu Sozeau | 2014-05-06 |
| * | Using hnf instead of "intro H" for forcing reduction to a product. |  herbelin | 2013-03-21 |
| * | Change Hint Resolve, Immediate to take a global reference as argument |  msozeau | 2012-10-26 |
| * | Updating headers. | herbelin | 2012-08-08 |
| * | Open Local Scope ---> Local Open Scope, same with Notation and alii |  letouzey | 2012-07-05 |
| * | Bug 2813 - Reflexive, Symmetric, Transitive instances for pointwise_relation ... |  pboutill | 2012-06-20 |
| * | Fixing tauto "special" behavior on singleton types w/ 2 parameters (bug #2680). | herbelin | 2012-04-15 |
| * | Fix interface of resolve_typeclasses: onlyargs -> with_goals: | msozeau | 2012-03-20 |
| * | Fix bugs related to Program integration. | msozeau | 2012-03-19 |
| * | Final part of moving Program code inside the main code. Adapted add_definitio... | msozeau | 2012-03-14 |
| * | Everything compiles again. | msozeau | 2012-03-14 |
| * | Revert "Tentative to fix bug #2628 by not letting intuition break records. Mi... | msozeau | 2012-01-31 |
| * | Tentative to fix bug #2628 by not letting intuition break records. Might be t... | msozeau | 2012-01-28 |
| * | Added the decidability of (<=) on nat. |  ppedrot | 2012-01-13 |
| * | Fixed the itarget of the previous commit... | ppedrot | 2012-01-06 |
| * | Added a typeclass-based system to reason on decidable propositions. | ppedrot | 2012-01-06 |
| * | theories/, plugins/ and test-suite/ ported to the Arguments vernacular |  gareuselesinge | 2011-11-21 |
| * | Merge subinstances branch by me and Tom Prince. | msozeau | 2011-11-17 |
| * | Fix bug #2586 and enhance clsubst* as well as a side effect | msozeau | 2011-10-18 |
| * | Proper fix for complement/flip instances. | msozeau | 2011-10-10 |
| * | Fix bug #2557 and an issue with Propers for complement | msozeau | 2011-10-07 |
| * | Use an ad-hoc monomorphic list in RelationClasses to avoid some universe cons... | letouzey | 2011-10-05 |
| * | Avoid registering λ and Π as keywords just for some private Local Notation | letouzey | 2011-09-06 |
| * | StrictOrder marked explicitly to be in Prop | letouzey | 2011-07-04 |
| * | Merge branch 'subclasses' into coq-trunk | msozeau | 2011-05-05 |
| * | - Add modulo_delta_types flag for unification to allow full | msozeau | 2011-03-13 |
| * | - Allow rewriting under abitrary products, not just those in Prop. | msozeau | 2011-02-28 |
| * | Add [Typeclasses Debug] option that respects backtracking, solve | msozeau | 2011-01-11 |
| * | f_equiv : a clone of f_equal that handles setoid equivalences | letouzey | 2011-01-04 |
| * | Numbers: some improvements in proofs | letouzey | 2011-01-03 |
| * | First release of Vector library. | pboutill | 2010-12-10 |
| * | In passing, very quick uniformization of coqdoc headers in a few files. | herbelin | 2010-12-09 |
| * | Fixed commit r13359 which was incomplete for its "trunk" part. Thanks | herbelin | 2010-07-31 |
| * | Minor fixes: | msozeau | 2010-07-27 |
| * | Updated all headers for 8.3 and trunk | herbelin | 2010-07-24 |
| * | Made option "Automatic Introduction" active by default before too many | herbelin | 2010-06-08 |
| * | 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 |
| * | RelationClasses: adapt eq_Reflexive and co to avoid Universe Inconsistencies | letouzey | 2010-02-17 |
Jason Gross
Matthieu Sozeau
Pierre Letouzey
Matthieu Sozeau
herbelin
msozeau
letouzey
pboutill
ppedrot
gareuselesinge
aspiwack