| Commit message (Expand) | Author | Age | |
|---|---|---|---|
| * | MSets: Class Ok becomes a definition instead of an inductive (thanks Matthieu) |  letouzey | 2010-01-12 |
| * | MSetAVL: hints made local since some of them are quite violent (transitivity) | letouzey | 2010-01-07 |
| * | Avoid declaring hints about refl/sym/trans of eq in DecidableType2 | letouzey | 2010-01-05 |
| * | Fix [Instance: forall ..., C args := t] declarations to behave as |  msozeau | 2009-11-15 |
| * | Use generalizable variables info when internalizing arbitrary bindings, | msozeau | 2009-11-08 |
| * | Better visibility of the inductive CompSpec used to specify comparison functions | letouzey | 2009-11-03 |
| * | OrderedType implementation for various numerical datatypes + min/max structures | letouzey | 2009-11-03 |
| * | OrderedType2 : trivial lemmas are turned into tests for order. | letouzey | 2009-10-16 |
| * | MSets: a new generation of FSets | letouzey | 2009-10-13 |
 |
index : coq | |
| the Coq proof assistant |
| aboutsummaryrefslogtreecommitdiffhomepage |