| Commit message (Expand) | Author | Age |
|---|
| * | 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 |
| * | Use an ad-hoc monomorphic list in RelationClasses to avoid some universe cons... |  letouzey | 2011-10-05 |
| * | StrictOrder marked explicitly to be in Prop | letouzey | 2011-07-04 |
| * | Add [Typeclasses Debug] option that respects backtracking, solve | msozeau | 2011-01-11 |
| * | In passing, very quick uniformization of coqdoc headers in a few files. |  herbelin | 2010-12-09 |
| * | Minor fixes: | msozeau | 2010-07-27 |
| * | 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 |
| * | RelationClasses: adapt eq_Reflexive and co to avoid Universe Inconsistencies | letouzey | 2010-02-17 |
| * | ZBinary (impl of Numbers via Z) reworked, comes earlier, subsumes ZOrderedType | letouzey | 2010-02-09 |
| * | Support "Local Obligation Tactic" (now the default in sections). | msozeau | 2010-01-11 |
| * | Use generalizable variables info when internalizing arbitrary bindings, | msozeau | 2009-11-08 |
| * | list, length, app are migrated from List to Datatypes | letouzey | 2009-11-02 |
| * | Add a new vernacular command for controling implicit generalization of | msozeau | 2009-10-27 |
| * | Fix new instances that could easily make class resolution loop on | msozeau | 2009-10-22 |
| * | MSets: a new generation of FSets | letouzey | 2009-10-13 |
| * | Correctly do backtracking during type class resolution even if only new | msozeau | 2009-10-05 |
| * | Fix the stdlib doc compilation + switch all .v file to utf8 | letouzey | 2009-09-28 |
| * | Delete trailing whitespaces in all *.{v,ml*} files |  glondu | 2009-09-17 |
| * | Stop using [obligation_tactic] from Program.Tactics as the default | msozeau | 2009-09-15 |
| * | Misc fixes: | msozeau | 2009-09-10 |
| * | Fix the bug-ridden code used to choose leibniz or generalized | msozeau | 2009-09-08 |
| * | Minor fixes in typeclasses: | msozeau | 2009-05-16 |
| * | - Implementation of a new typeclasses eauto procedure based on success | msozeau | 2009-04-27 |
| * | Better Requires in Classes. Fix bug #2093: the code does not require | msozeau | 2009-04-16 |
| * | Move setoid_rewrite to its own module and do some clean up in | msozeau | 2009-04-07 |
| * | Rewrite of Program Fixpoint to overcome the previous limitations: | msozeau | 2009-03-28 |
| * | Fix [subrelation] clauses that privileged the weakest. Better impl args | msozeau | 2009-02-04 |
| * | Last changes in type class syntax: | msozeau | 2009-01-18 |
| * | Generalized binding syntax overhaul: only two new binders: `() and `{}, | msozeau | 2008-12-14 |
| * | Generalized implementation of generalization. | msozeau | 2008-10-23 |
| * | Use manual implicts in Classes and rationalize class parameter names. | msozeau | 2008-09-14 |
| * | Add enough information to correctly globalize recursive calls in inductive and | msozeau | 2008-09-11 |
| * | Add the ability to declare [Hint Extern]'s with no pattern. | msozeau | 2008-09-07 |
| * | Improve typeclasses eauto using the dnet for local assumptions too, and select | msozeau | 2008-09-04 |
| * | Fix bug #1935, reworking the reflexivity, symmetry... tactics to use | msozeau | 2008-09-03 |
| * | Major speed and space improvements in setoid rewrite: | msozeau | 2008-08-27 |
| * | - New auto hints for transparency/opacity control, not bound to | msozeau | 2008-08-22 |
| * | New tactics [conv] to test convertibility (actually, unification) of two | msozeau | 2008-07-22 |
| * | - Improve [Context] vernacular to allow arbitrary binders, not just | msozeau | 2008-07-07 |
| * | Fixes in handling of implicit arguments: | msozeau | 2008-07-04 |
| * | Enhanced discrimination nets implementation, which can now work with | msozeau | 2008-06-27 |
| * | Rename obligations_tactic to obligation_tactic and fix bugs #1893. | msozeau | 2008-06-22 |
| * | - Correct handling of DependentMorphism error, using tclFAIL instead of | msozeau | 2008-06-10 |
| * | - Extension de "generalize" en "generalize c as id at occs". | herbelin | 2008-06-08 |
| * | - Cleanup parsing of binders, reducing to a single production for all | msozeau | 2008-05-11 |
| * | Fix eauto still using delta when it shouldn't (should make CoRN compile | msozeau | 2008-04-29 |
| * | More renamings to avoid clashes (e.g. with CoRN). | msozeau | 2008-04-15 |
gareuselesinge
msozeau
letouzey
herbelin
aspiwack
glondu