aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/MSets/MSetInterface.v
Commit message (Expand)AuthorAge
* 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-07-06 03:01:57 +0000