aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/MSets/MSetInterface.v
Commit message (Expand)AuthorAge
* Typeclasses: stdlib fixes for new search algorithmGravatar Matthieu Sozeau2016-06-16
* Restore implicit arguments of irreflexivity (fixes bug #3305).Gravatar Matthieu Sozeau2014-05-09
* This commit adds full universe polymorphism and fast projections to Coq.Gravatar Matthieu Sozeau2014-05-06
* "Boolean Equality" and "Case Analysis" are already off by default...Gravatar letouzey2013-07-17
* induction/destruct : nicer syntax for generating equations (solves #2741)Gravatar letouzey2012-07-09
* theories/, plugins/ and test-suite/ ported to the Arguments vernacularGravatar gareuselesinge2011-11-21
* - Add modulo_delta_types flag for unification to allow fullGravatar msozeau2011-03-13
* FSets/Msets: some renaming of module params to simplify the task of the extra...Gravatar letouzey2010-07-05
* MSetInterface: no induction principle about a Record (nicer extraction)Gravatar letouzey2010-06-16
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* 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
* Include can accept both Module and Module TypeGravatar letouzey2010-01-07
* MSetInterface: more modularityGravatar letouzey2010-01-07
* Avoid declaring hints about refl/sym/trans of eq in DecidableType2Gravatar letouzey2010-01-05
* Specific syntax for Instances in Module Type: Declare InstanceGravatar letouzey2010-01-04
* Fix backtracking heuristic in typeclass resolution. Gravatar msozeau2009-11-30
* 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
* MSetInterface: some explicit types to avoid Raw.t-instead-of-t effectGravatar letouzey2009-10-21
* Structure/OrderTac.v : highlight the "order" tactic by isolating it from FSet...Gravatar letouzey2009-10-16
* MSetInterface: (W)Raw2Sets splitted in 2 (helps a future commit by Elie)Gravatar letouzey2009-10-15
* OrderedType2.order is slightly weaker since last commit, adapt accordinglyGravatar letouzey2009-10-15
* MSets: a new generation of FSetsGravatar letouzey2009-10-13
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-11 18:43:03 +0000