aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/MSets/MSetWeakList.v
Commit message (Expand)AuthorAge
* - Add modulo_delta_types flag for unification to allow fullGravatar msozeau2011-03-13
* Made option "Automatic Introduction" active by default before too manyGravatar herbelin2010-06-08
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* MSets: Class Ok becomes a definition instead of an inductive (thanks Matthieu)Gravatar letouzey2010-01-12
* Avoid declaring hints about refl/sym/trans of eq in DecidableType2Gravatar letouzey2010-01-05
* Fix [Instance: forall ..., C args := t] declarations to behave asGravatar msozeau2009-11-15
* Use generalizable variables info when internalizing arbitrary bindings,Gravatar msozeau2009-11-08
* MSets: a new generation of FSetsGravatar letouzey2009-10-13