coq - The formal proof system

Age	Commit message (Expand)	Author
2010-02-12	CompSpecType, a clone of CompSpec but in Type instead of Prop	letouzey
2010-01-12	MSets: Class Ok becomes a definition instead of an inductive (thanks Matthieu)	letouzey
2010-01-07	Nicer names: DecidableType2* --> Equalities, OrderedType2 --> Orders*	letouzey
2010-01-07	Include can accept both Module and Module Type	letouzey
2010-01-07	MSetInterface: more modularity	letouzey
2010-01-07	MSetAVL: hints made local since some of them are quite violent (transitivity)	letouzey
2010-01-05	Avoid declaring hints about refl/sym/trans of eq in DecidableType2	letouzey
2010-01-04	Specific syntax for Instances in Module Type: Declare Instance	letouzey
2009-12-09	Factorisation between Makefile and ocamlbuild systems : .vo to compile are in...	letouzey
2009-12-08	integrate MSetToFiniteSet into the compilation (and fix it)	letouzey
2009-11-30	Fix backtracking heuristic in typeclass resolution.	msozeau
2009-11-15	Fix [Instance: forall ..., C args := t] declarations to behave as	msozeau
2009-11-08	Use generalizable variables info when internalizing arbitrary bindings,	msozeau
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-10-27	Add a new vernacular command for controling implicit generalization of	msozeau
2009-10-21	MSetInterface: some explicit types to avoid Raw.t-instead-of-t effect	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	MSetInterface: (W)Raw2Sets splitted in 2 (helps a future commit by Elie)	letouzey
2009-10-15	OrderedType2.order is slightly weaker since last commit, adapt accordingly	letouzey
2009-10-13	MSets: a new generation of FSets	letouzey