coq - The formal proof system

Age	Commit message (Expand)	Author
2009-12-02	Remove interface plugin	glondu
2009-11-27	Added support for definition of fixpoints using tactics.	herbelin
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-11	Added support for multiple where-clauses in Inductive and co (see wish #2163).	herbelin
2009-11-04	Fixed record syntax "{\|x=...; y=...\|}" so that it works with qualified names.	gmelquio
2009-10-28	Integrate a few improvements on typeclasses and Program from the equations br...	msozeau
2009-10-27	Add a new vernacular command for controling implicit generalization of	msozeau
2009-10-26	New cleaning phase of the Local/Global option management	herbelin
2009-09-29	Add support for Local Declare ML Module	glondu
2009-09-20	Only one "in" clause in "destruct" even for a multiple "destruct".	herbelin
2009-09-17	Delete trailing whitespaces in all .{v,ml} files	glondu
2009-09-11	Generalized the possibility to refer to a global name by a notation	herbelin
2009-09-10	Added syntax "exists bindings, ..., bindings" for iterated "exists".	herbelin
2009-08-14	+Fix interface.	aspiwack
2009-08-11	Infix (r12268 continued)	herbelin
2009-08-03	Added "etransitivity".	herbelin
2009-08-02	Improved parameterization of Coq:	herbelin
2009-07-24	Remove the barely-used/obsolete/undocumented syntax "conditional <tac> rewrite"	letouzey
2009-06-29	Miscellaneous practical commits:	herbelin
2009-04-27	- Cleaning (unification of ML names, removal of obsolete code,	herbelin
2009-03-20	Directory 'contrib' renamed into 'plugins', to end confusion with archive of ...	letouzey