aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Structures
Commit message (Expand)AuthorAge
...
* DecidableType2+OrderedType2 : notations in specific Module Type, slicing of O...Gravatar letouzey2010-01-07
* misc improvements in some Structures filesGravatar 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
* RelationPairs: stop loading it in all Numbers, stop maximal args with fst/sndGravatar letouzey2009-12-18
* Reverse order of arguments in min_case_strong for better uniformity (and comp...Gravatar letouzey2009-12-17
* Factorisation between Makefile and ocamlbuild systems : .vo to compile are in...Gravatar letouzey2009-12-09
* No more specific syntax "Include Self" for inclusion of partially-applied fun...Gravatar letouzey2009-12-07
* Minor fixes in typeclasses, avoiding repeated evar normalizations.Gravatar msozeau2009-11-24
* Module subtyping : allow many <: and module type declaration with <:Gravatar letouzey2009-11-18
* New syntax <+ for chains of Include (or Include Type) (or Include Self (Type))Gravatar letouzey2009-11-16
* Taking advantage of the new "Include Self Type" in DecidableType2 and NZAxiomsGravatar letouzey2009-11-16
* Simplification of Numbers, mainly thanks to IncludeGravatar letouzey2009-11-10
* DecidableType: A specification via boolean equality as an alternative to eq_decGravatar letouzey2009-11-10
* 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
* List + SetoidList : some cleanup around predicates Exists, Forall, Forall2, F...Gravatar letouzey2009-11-02
* Add a new vernacular command for controling implicit generalization ofGravatar msozeau2009-10-27
* Improved the treatment of Local/Global options (noneffective Local onGravatar herbelin2009-10-25
* FSetCompat: a compatibility wrapper between FSets and MSetsGravatar letouzey2009-10-20
* Merge SetoidList2 into SetoidList: forgotten reference to the removed fileGravatar letouzey2009-10-19
* Merge SetoidList2 into SetoidList.Gravatar letouzey2009-10-19
* OrderedType2 : trivial lemmas are turned into tests for order.Gravatar letouzey2009-10-16
* Structure/OrderTac.v : highlight the "order" tactic by isolating it from FSet...Gravatar letouzey2009-10-16
* OrderedType2.order : fix the last fix (a fail at the wrong place)Gravatar letouzey2009-10-15
* Typo in last commitGravatar letouzey2009-10-14
* Improved tactic "order" in OrderedTypeGravatar letouzey2009-10-14
* MSets: a new generation of FSetsGravatar letouzey2009-10-13
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-12 09:24:00 +0000