coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Intuition: temporary(?) restore the unconditional unfolding of not	letouzey	2012-05-15
*	Fixing tauto "special" behavior on singleton types w/ 2 parameters (bug #2680).	herbelin	2012-04-15
*	Revert "Tentative to fix bug #2628 by not letting intuition break records. Mi...	msozeau	2012-01-31
*	Tentative to fix bug #2628 by not letting intuition break records. Might be t...	msozeau	2012-01-28
*	theories/, plugins/ and test-suite/ ported to the Arguments vernacular	gareuselesinge	2011-11-21
*	MSet/FSet/FMap : add more explicitly an alternative spec for fold via fold_right	letouzey	2011-10-14
*	Fix compilation issues.	msozeau	2011-02-16
*	- Fix treatment of globality flag for typeclass instance hints (they	msozeau	2011-02-14
*	Cosmetic : let's take advantage of the n-ary exists notation	letouzey	2010-12-17
*	FMapFacts: typo noticed by Aaron	letouzey	2010-10-22
*	Remove the svn-specific $Id$ annotations	letouzey	2010-04-29
*	List + SetoidList : some cleanup around predicates Exists, Forall, Forall2, F...	letouzey	2009-11-02
*	Merge SetoidList2 into SetoidList.	letouzey	2009-10-19
*	Init/Tactics.v: tactic with nicer name 'exfalso' for 'elimtype False'	letouzey	2009-10-08
*	Implicit argument of Logic.eq become maximally inserted	letouzey	2009-10-08
*	Delete trailing whitespaces in all .{v,ml} files	glondu	2009-09-17
*	Fix the bug-ridden code used to choose leibniz or generalized	msozeau	2009-09-08
*	Simplify eauto and fix it for compatibility, allowing full delta during	msozeau	2009-07-14
*	Use the proper unification flags in e_exact. This makes exact fail a bit	msozeau	2009-07-09
*	Rename [Morphism] into [Proper] and [respect] into [proper] to comply	msozeau	2009-04-21
*	Just export RelationClasses for [Equivalence] through Setoid.	msozeau	2009-04-18
*	FMaps: various updates (mostly suggested by P. Casteran)	letouzey	2008-12-26
*	FMap: fold_rec + more permissive transpose hyp + various cleanup	letouzey	2008-12-22
*	FSet/OrderedType now includes an eq_dec, and hence become an extension of Dec...	letouzey	2008-12-17
*	Add user syntax for creating hint databases [Create HintDb foo	msozeau	2008-09-14
*	Correction du bug #1937	notin	2008-09-04
*	Enhanced discrimination nets implementation, which can now work with	msozeau	2008-06-27
*	Add the ability to specify what to do with free variables in instance	msozeau	2008-04-12
*	- A little cleanup in Classes/*. Separate standard morphisms on	msozeau	2008-04-08
*	Reorganize Program and Classes theories. Requiring Setoid no longer sets	msozeau	2008-03-16
*	f_equal, revert, specialize in ML, contradict in better Ltac (+doc)	letouzey	2008-03-07
*	repair FSets/FMap after the change in setoid rewrite	letouzey	2008-03-07
*	Plug the new setoid implemtation in, leaving the original one commented	msozeau	2008-03-06
*	migration from Set to Type of FSet/FMap + some dependencies...	letouzey	2008-03-04
*	A fix for compilation of FMapFacts (a story of impl arg for Logic.eq)	letouzey	2008-03-02
*	Some suggestions about FMap by P. Casteran:	letouzey	2008-02-28
*	cardinal is promoted to the rank of primitive member of the FMap interface	letouzey	2008-02-28
*	Reorganization of FSet+FMap : no more files specific to Weak Sets/Maps	letouzey	2008-02-04
*	more user-friendly versions of some properties lemmas in FSets/FMap	letouzey	2008-01-04
*	small tactics "swap" and "absurd_hyp" are now obsolete: "contradict" is	letouzey	2007-11-06
*	Cleanup attempt of Hints in *Interface.v files.	letouzey	2007-10-21
*	- Extensions of FMap(Weak)Facts:	letouzey	2007-06-27
*	additional properties for FMap (and slight rework of SetoidList and FSetPrope...	letouzey	2007-06-26
*	Rework of FSetProperties, in order to add more easily a Properties functor	letouzey	2007-06-14
*	petits ajouts	letouzey	2006-05-31
*	un debut de propriétés concernant FMap	letouzey	2006-05-22