aboutsummaryrefslogtreecommitdiff
path: root/theories/MSets/MSetWeakList.v
AgeCommit message (Expand)Author
2016-11-24Fix some documentation typos.Guillaume Melquiond
2014-06-01Making those proofs which depend on names generated for the argumentsHugo Herbelin
2014-05-02Eta contractions to please cbnPierre Boutillier
2012-10-26Change Hint Resolve, Immediate to take a global reference as argumentmsozeau
2012-07-09induction/destruct : nicer syntax for generating equations (solves #2741)letouzey
2011-03-13- Add modulo_delta_types flag for unification to allow fullmsozeau
2010-06-08Made option "Automatic Introduction" active by default before too manyherbelin
2010-04-29Remove the svn-specific $Id$ annotationsletouzey
2010-01-12MSets: Class Ok becomes a definition instead of an inductive (thanks Matthieu)letouzey
2010-01-05Avoid declaring hints about refl/sym/trans of eq in DecidableType2letouzey
2009-11-15Fix [Instance: forall ..., C args := t] declarations to behave asmsozeau
2009-11-08Use generalizable variables info when internalizing arbitrary bindings,msozeau
2009-10-13MSets: a new generation of FSetsletouzey
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-20 21:57:57 +0000