aboutsummaryrefslogtreecommitdiff
path: root/theories/Structures/DecidableType2.v
AgeCommit message (Expand)Author
2010-01-07Nicer names: DecidableType2* --> Equalities*, OrderedType2* --> Orders*letouzey
2010-01-07DecidableType2+OrderedType2 : notations in specific Module Type, slicing of O...letouzey
2010-01-05Avoid declaring hints about refl/sym/trans of eq in DecidableType2letouzey
2010-01-04Specific syntax for Instances in Module Type: Declare Instanceletouzey
2009-12-07No more specific syntax "Include Self" for inclusion of partially-applied fun...letouzey
2009-11-18Module subtyping : allow many <: and module type declaration with <:letouzey
2009-11-16New syntax <+ for chains of Include (or Include Type) (or Include Self (Type))letouzey
2009-11-16Taking advantage of the new "Include Self Type" in DecidableType2 and NZAxiomsletouzey
2009-11-10Simplification of Numbers, mainly thanks to Includeletouzey
2009-11-10DecidableType: A specification via boolean equality as an alternative to eq_decletouzey
2009-11-03OrderedType implementation for various numerical datatypes + min/max structuresletouzey
2009-10-25Improved the treatment of Local/Global options (noneffective Local onherbelin
2009-10-20FSetCompat: a compatibility wrapper between FSets and MSetsletouzey
2009-10-19Merge SetoidList2 into SetoidList: forgotten reference to the removed fileletouzey
2009-10-13MSets: a new generation of FSetsletouzey
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-02 02:51:24 +0000