coq - The formal proof system

Age	Commit message (Expand)	Author
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-28	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-27	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-26	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-25	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-24	Fixing XML doc (COQ_XML not working as an environment variable).	herbelin
2009-10-23	First debug... the renaming of librairies was not working and auto/dn were no...	soubiran
2009-10-22	Fix new instances that could easily make class resolution loop on	msozeau
2009-10-21	This big commit addresses two problems:	soubiran
2009-10-21	MSetInterface: some explicit types to avoid Raw.t-instead-of-t effect	letouzey
2009-10-20	Repaired bug #2165 (buggy coq example in Tactic Examples doc chapter)	herbelin
2009-10-20	Added syntactic coloration for 'Function'.	gmelquio
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-17	Fixed a notation bug when extending binder_constr with empty levels	herbelin
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-16	note for later : when the tag table is shared, never, ever create two	vgross
2009-10-15	typo in doc of Extraction Blacklist	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-15	OrderedType2.order : fix the last fix (a fail at the wrong place)	letouzey
2009-10-15	Fix bug in typeclass resolution discoverd by Eeelis van der Weegen:	msozeau
2009-10-14	Typo in last commit	letouzey
2009-10-14	Improved tactic "order" in OrderedType	letouzey