coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
*	Module subtyping : allow many <: and module type declaration with <:	letouzey	2009-11-18
*	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-16
*	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-10
*	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-03
*	List + SetoidList : some cleanup around predicates Exists, Forall, Forall2, F...	letouzey	2009-11-02
*	Add a new vernacular command for controling implicit generalization of	msozeau	2009-10-27
*	Improved the treatment of Local/Global options (noneffective Local on	herbelin	2009-10-25
*	FSetCompat: a compatibility wrapper between FSets and MSets	letouzey	2009-10-20
*	Merge SetoidList2 into SetoidList: forgotten reference to the removed file	letouzey	2009-10-19
*	Merge SetoidList2 into SetoidList.	letouzey	2009-10-19
*	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-16
*	OrderedType2.order : fix the last fix (a fail at the wrong place)	letouzey	2009-10-15
*	Typo in last commit	letouzey	2009-10-14
*	Improved tactic "order" in OrderedType	letouzey	2009-10-14
*	MSets: a new generation of FSets	letouzey	2009-10-13