aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/MSets/MSetWeakList.v
Commit message (Expand)AuthorAge
* Update headers following #6543.Gravatar Théo Zimmermann2018-02-27
* Fix some documentation typos.Gravatar Guillaume Melquiond2016-11-24
* Making those proofs which depend on names generated for the argumentsGravatar Hugo Herbelin2014-06-01
* Eta contractions to please cbnGravatar Pierre Boutillier2014-05-02
* Change Hint Resolve, Immediate to take a global reference as argumentGravatar msozeau2012-10-26
* induction/destruct : nicer syntax for generating equations (solves #2741)Gravatar letouzey2012-07-09
* - 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-25 22:28:37 +0000