coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Update headers following #6543.	Théo Zimmermann	2018-02-27
*	Prelude : no more autoload of plugins extraction and recdef	Pierre Letouzey	2017-06-14
*	Simpl less (so that cbn will not simpl too much)	Pierre Boutillier	2014-10-01
*	instanciation is French, instantiation is English	Jason Gross	2014-08-25
*	Grammar: "allowing to" is not proper English	Jason Gross	2014-08-25
*	Avoid using a deprecated lemma in the standard library.	Guillaume Melquiond	2014-06-26
*	Making those proofs which depend on names generated for the arguments	Hugo Herbelin	2014-06-01
*	This commit adds full universe polymorphism and fast projections to Coq.	Matthieu Sozeau	2014-05-06
*	Unset Asymmetric Patterns	pboutill	2013-01-18
*	No more constant named "int" in Coq theories (cf bug #2878)	letouzey	2012-12-18
*	Ltac repeat is in fact already doing progress	letouzey	2012-10-01
*	Kills the useless tactic annotations "in \|- *"	letouzey	2012-07-05
*	Open Local Scope ---> Local Open Scope, same with Notation and alii	letouzey	2012-07-05
*	Modularization of BinInt, related fixes in the stdlib	letouzey	2011-05-05
*	- Use transparency information all the way through unification and	msozeau	2011-02-17
*	s/appartness/membership/g (Closes: #2470)	glondu	2011-01-06
*	Extraction: re-introduce some eta-expansions in rare situations leading to '_...	letouzey	2010-09-20
*	For the moment, two small manual eta-expansions to avoid '_a after extraction	letouzey	2010-09-17
*	Made option "Automatic Introduction" active by default before too many	herbelin	2010-06-08
*	Remove the svn-specific $Id$ annotations	letouzey	2010-04-29
*	Merge SetoidList2 into SetoidList.	letouzey	2009-10-19
*	Structure/OrderTac.v : highlight the "order" tactic by isolating it from FSet...	letouzey	2009-10-16
*	Fix the stdlib doc compilation + switch all .v file to utf8	letouzey	2009-09-28
*	Delete trailing whitespaces in all .{v,ml} files	glondu	2009-09-17
*	made several occurrences of (eapply ...; eauto) not rely on the lack of patte...	barras	2009-06-22
*	Intropattern: syntax {x,y,z,t} becomes (x & y & z & t), as decided in	letouzey	2008-06-01
*	Prevent the apparition of &&& when printing a (if ... then ... else false)	letouzey	2008-04-17
*	New file FMapFullAVL containing the balancing proofs about FMapAVL:	letouzey	2008-04-03
*	Rework of FMapAVL inspired by recent changes of FSetAVL:	letouzey	2008-04-03
*	Reorganisation of FSetAVL (consequences of remarks by B. Gregoire)	letouzey	2008-03-15
*	repair FSets/FMap after the change in setoid rewrite	letouzey	2008-03-07
*	migration from Set to Type of FSet/FMap + some dependencies...	letouzey	2008-03-04
*	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
*	Major revision: use of Function, including some non-structural ones	letouzey	2008-02-10
*	kill some useless module aliases E:=X (for better name printing, see Elie's 1...	letouzey	2008-02-05
*	small tactics "swap" and "absurd_hyp" are now obsolete: "contradict" is	letouzey	2007-11-06
*	Revision of the FSetWeak Interface, so that it becomes a precise	letouzey	2007-10-29
*	A generic preprocessing tactic zify for (r)omega	letouzey	2007-07-18
*	As suggested by Pierre Casteran, fold for FSets/FMaps now takes a	letouzey	2007-05-27
*	fix for bug #1347 (no more Scope pollution by FSets)	letouzey	2007-05-25
*	Passage des graphes de Function dans Type	jforest	2006-06-23
*	+ ameliorating the tactic "functional induction"	jforest	2006-06-06
*	Replacing the old version of "functional induction" with the new one.	jforest	2006-05-31
*	* suite de la revision des wrappers Make	letouzey	2006-05-30
*	suite de l'ajout des FSets/FMaps dans les theories standards	letouzey	2006-04-29