coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	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
*	Reverted an incorrect code simplification in function status_changed	herbelin	2009-11-02
*	List + SetoidList : some cleanup around predicates Exists, Forall, Forall2, F...	letouzey	2009-11-02
*	Remove various useless {struct} annotations	letouzey	2009-11-02
*	Added alternate versions of existing lemmas on sqrt.	gmelquio	2009-11-02
*	Correction du bug #2175	notin	2009-11-02
*	Sorting/Permutation: no need to require the whole Arith (and hence plugins li...	letouzey	2009-11-02
*	Operators_Properties: avoid to depend on Setoid	letouzey	2009-11-02
*	list, length, app are migrated from List to Datatypes	letouzey	2009-11-02
*	Undo 12432 which caused an exponential behavior at Requires. Compilation time...	puech	2009-10-30
*	Attempt to capture on time unification errors for "with" bindings.	herbelin	2009-10-30
*	Take constraints into account in the "instantiate" tactic	herbelin	2009-10-30
*	Added Coqide highlighting for extraction vernacular.	gmelquio	2009-10-30
*	Removed 'dest' from keyword highlighting.	gmelquio	2009-10-30
*	Hopefully improved layout of fix guardness error message.	herbelin	2009-10-29
*	Fix flat_map definition so that it plays nicely with fix	glondu	2009-10-29
*	Fixed some typos in the reference manual.	gmelquio	2009-10-29
*	Revision 12439 continued, printing part (notations to names behave	herbelin	2009-10-29
*	Fix bug in dnet.ml, which missed some results when filtering one term against...	puech	2009-10-29
*	Integrate a few improvements on typeclasses and Program from the equations br...	msozeau	2009-10-28
*	Made that notations to names behave like the names they refer to wrt	herbelin	2009-10-28
*	Fixed a bug when reporting unexisting reference to an inductive	herbelin	2009-10-28
*	Clarification in comments	glondu	2009-10-28
*	Remove old compatibility stuff (Tacred.nf)	glondu	2009-10-28
*	Make usage of Dyn explicit	glondu	2009-10-28
*	Backport fix for indexing of sorts which collapse every Type occurrence	msozeau	2009-10-28
*	Typo in the refman	puech	2009-10-28
*	Fix incorrect registration of objects in libtypes.ml when defining a module.	puech	2009-10-28
*	Same as commit 12430 but with the good version of the function iter_all_segment	soubiran	2009-10-28
*	From now SearchAbout requests search also inside INCLUDE libobject.	soubiran	2009-10-28
*	Module type expressions of the form (Fsig X) with Definition foo := bar are n...	soubiran	2009-10-28
*	Add a new vernacular command for controling implicit generalization of	msozeau	2009-10-27
*	Fixes around typeclasses:	msozeau	2009-10-27
*	Added option --external to coqdoc to bind an url to an external library.	herbelin	2009-10-27
*	Documentation of the Local and Global modifiers.	herbelin	2009-10-27
*	fix previous commit	corbinea	2009-10-27
*	fixed czar bug with parametric inductives	corbinea	2009-10-27
*	Fix Setoid documentation.	msozeau	2009-10-26
*	Local/Global revision 12418 continued	herbelin	2009-10-26
*	Adapted test unfold.v after eq gets its argument maximally inserted	herbelin	2009-10-26
*	New cleaning phase of the Local/Global option management	herbelin	2009-10-26
*	New functors for gmap and gset.	soubiran	2009-10-26
*	Restore (and test) broken chaining of lemmas in "apply in" in presence	herbelin	2009-10-25
*	fixed bug in Czar grammar	corbinea	2009-10-25
*	Add support for remaining side-conditions in "apply in as".	herbelin	2009-10-25
*	Improved the treatment of Local/Global options (noneffective Local on	herbelin	2009-10-25
*	Fixing XML doc (COQ_XML not working as an environment variable).	herbelin	2009-10-24
*	First debug... the renaming of librairies was not working and auto/dn were no...	soubiran	2009-10-23
*	Fix new instances that could easily make class resolution loop on	msozeau	2009-10-22