| Commit message (Expand) | Author | Age |
|---|
| * | 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 |
| * | Cleanup in Classes, removing unsupported code. | msozeau | 2010-02-11 |
| * | ZBinary (impl of Numbers via Z) reworked, comes earlier, subsumes ZOrderedType | letouzey | 2010-02-09 |
| * | Update CHANGES, add documentation for new commands/tactics and do a bit | msozeau | 2010-01-30 |
| * | Support for generalized rewriting under dependent binders, using the | msozeau | 2010-01-26 |
| * | Support "Local Obligation Tactic" (now the default in sections). | msozeau | 2010-01-11 |
| * | RelationPairs: stop loading it in all Numbers, stop maximal args with fst/snd | letouzey | 2009-12-18 |
| * | Factorisation between Makefile and ocamlbuild systems : .vo to compile are in... | letouzey | 2009-12-09 |
| * | Rename proper to proper_prf to avoid clash with CoRN, | msozeau | 2009-12-03 |
| * | Fix backtracking heuristic in typeclass resolution. | msozeau | 2009-11-30 |
| * | Added support for definition of fixpoints using tactics. | herbelin | 2009-11-27 |
| * | Document Generalizable Variables, and change syntax to | msozeau | 2009-11-15 |
| * | Use generalizable variables info when internalizing arbitrary bindings, | msozeau | 2009-11-08 |
herbelin
msozeau
letouzey
pboutill
ppedrot
gareuselesinge
aspiwack