coq - The formal proof system

Age	Commit message (Expand)	Author
2009-12-09	Factorisation between Makefile and ocamlbuild systems : .vo to compile are in...	letouzey
2009-12-07	No more specific syntax "Include Self" for inclusion of partially-applied fun...	letouzey
2009-11-24	Minor fixes in typeclasses, avoiding repeated evar normalizations.	msozeau
2009-11-18	Module subtyping : allow many <: and module type declaration with <:	letouzey
2009-11-16	New syntax <+ for chains of Include (or Include Type) (or Include Self (Type))	letouzey
2009-11-16	Taking advantage of the new "Include Self Type" in DecidableType2 and NZAxioms	letouzey
2009-11-10	Simplification of Numbers, mainly thanks to Include	letouzey
2009-11-10	DecidableType: A specification via boolean equality as an alternative to eq_dec	letouzey
2009-11-03	Better visibility of the inductive CompSpec used to specify comparison functions	letouzey
2009-11-03	OrderedType implementation for various numerical datatypes + min/max structures	letouzey
2009-11-02	List + SetoidList : some cleanup around predicates Exists, Forall, Forall2, F...	letouzey
2009-10-27	Add a new vernacular command for controling implicit generalization of	msozeau
2009-10-25	Improved the treatment of Local/Global options (noneffective Local on	herbelin
2009-10-20	FSetCompat: a compatibility wrapper between FSets and MSets	letouzey
2009-10-19	Merge SetoidList2 into SetoidList: forgotten reference to the removed file	letouzey
2009-10-19	Merge SetoidList2 into SetoidList.	letouzey
2009-10-16	OrderedType2 : trivial lemmas are turned into tests for order.	letouzey
2009-10-16	Structure/OrderTac.v : highlight the "order" tactic by isolating it from FSet...	letouzey
2009-10-15	OrderedType2.order : fix the last fix (a fail at the wrong place)	letouzey
2009-10-14	Typo in last commit	letouzey
2009-10-14	Improved tactic "order" in OrderedType	letouzey
2009-10-13	MSets: a new generation of FSets	letouzey