aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/MSets/MSetList.v
Commit message (Expand)AuthorAge
* Update headers following #6543.Gravatar Théo Zimmermann2018-02-27
* Fix some documentation typos.Gravatar Guillaume Melquiond2016-11-24
* Revert "Temporary hack to compensate missing comma while re-printing tactic"Gravatar Hugo Herbelin2016-04-27
* Temporary hack to compensate missing comma while re-printing tacticGravatar Hugo Herbelin2016-04-27
* Try a new way of handling template universe levelsGravatar Matthieu Sozeau2014-05-06
* This commit adds full universe polymorphism and fast projections to Coq.Gravatar Matthieu Sozeau2014-05-06
* 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
* Made notations for exists, exists! and notations of Utf8.v recursive notationsGravatar herbelin2010-07-22
* Made option "Automatic Introduction" active by default before too manyGravatar herbelin2010-06-08
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* Change definition of FSetList so that equality is LeibnizGravatar glondu2010-04-09
* CompSpecType, a clone of CompSpec but in Type instead of PropGravatar letouzey2010-02-12
* MSets: Class Ok becomes a definition instead of an inductive (thanks Matthieu)Gravatar letouzey2010-01-12
* Nicer names: DecidableType2* --> Equalities*, OrderedType2* --> Orders*Gravatar letouzey2010-01-07
* 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
* Better visibility of the inductive CompSpec used to specify comparison functionsGravatar letouzey2009-11-03
* OrderedType implementation for various numerical datatypes + min/max structuresGravatar letouzey2009-11-03
* Structure/OrderTac.v : highlight the "order" tactic by isolating it from FSet...Gravatar letouzey2009-10-16
* OrderedType2.order is slightly weaker since last commit, adapt accordinglyGravatar letouzey2009-10-15
* MSets: a new generation of FSetsGravatar letouzey2009-10-13