aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/MSets/MSetAVL.v
Commit message (Expand)AuthorAge
* Removing "intro" from the tactic AST.Gravatar Pierre-Marie Pédrot2016-06-03
* ZArith/Int.v: some modernizationsGravatar Pierre Letouzey2015-04-02
* "allows to", like "allowing to", is improperGravatar Jason Gross2014-08-25
* "Boolean Equality" and "Case Analysis" are already off by default...Gravatar letouzey2013-07-17
* No more constant named "int" in Coq theories (cf bug #2878)Gravatar letouzey2012-12-18
* Change Hint Resolve, Immediate to take a global reference as argumentGravatar msozeau2012-10-26
* MSetRBT : implementation of MSets via Red-Black treesGravatar letouzey2012-04-13
* MSetAVL: better implementation of filter suggested by X. LeroyGravatar letouzey2012-01-17
* theories/, plugins/ and test-suite/ ported to the Arguments vernacularGravatar gareuselesinge2011-11-21
* Modularization of BinInt, related fixes in the stdlibGravatar letouzey2011-05-05
* CompareSpec: a slight generalization/reformulation of CompSpecGravatar letouzey2011-03-17
* - Use transparency information all the way through unification andGravatar msozeau2011-02-17
* s/appartness/membership/g (Closes: #2470)Gravatar glondu2011-01-06
* Extraction: re-introduce some eta-expansions in rare situations leading to '_...Gravatar letouzey2010-09-20
* For the moment, two small manual eta-expansions to avoid '_a after extractionGravatar letouzey2010-09-17
* Made notations for exists, exists! and notations of Utf8.v recursive notationsGravatar herbelin2010-07-22
* MSetAVL: for nicer extraction, we create only tree_ind, not tree_rect and tre...Gravatar letouzey2010-06-15
* 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
* MSetAVL: hints made local since some of them are quite violent (transitivity)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
* OrderedType2 : trivial lemmas are turned into tests for order.Gravatar letouzey2009-10-16
* MSets: a new generation of FSetsGravatar letouzey2009-10-13