coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Ltac repeat is in fact already doing progress	letouzey	2012-10-01
*	No more states/initial.coq, instead coqtop now requires Prelude.vo	letouzey	2012-08-23
*	fast bitwise operations (lor,land,lxor) on int31 and BigN	letouzey	2012-08-11
*	Updating headers.	herbelin	2012-08-08
*	MSetRBT: a tail-recursive plength	letouzey	2012-08-06
*	Same for Fin	pboutill	2012-07-25
*	Vector equalities first stuff	pboutill	2012-07-20
*	isolate instances about Permutation and PermutationA which may slow rewrite	letouzey	2012-07-10
*	induction/destruct : nicer syntax for generating equations (solves #2741)	letouzey	2012-07-09
*	Two adaptations after the changes of level of ->	letouzey	2012-07-06
*	BinPos/BinInt/BinNat : fix some argument scopes	letouzey	2012-07-06
*	Restore the compatibility notation Compare.not_eq_sym	letouzey	2012-07-06
*	Legacy Ring and Legacy Field migrated to contribs	letouzey	2012-07-05
*	Some cleanup in recent proofs concerning pi	letouzey	2012-07-05
*	MSetRBT : elementary arith proofs instead of calls to lia	letouzey	2012-07-05
*	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
*	ZArith + other : favor the use of modern names instead of compat notations	letouzey	2012-07-05
*	Notation: a new annotation "compat 8.x" extending "only parsing"	letouzey	2012-07-05
*	Bug 2813 - Reflexive, Symmetric, Transitive instances for pointwise_relation ...	pboutill	2012-06-20
*	Fix bug #2695: infinite loop in dependent destruction.	msozeau	2012-06-19
*	BinInt: a forgotten scope for a notation	letouzey	2012-06-19
*	These files are displaced from Rtrigo.v and Ranalysis_reg.v	bertot	2012-06-11
*	finish the rearrangement for removing the sin_PI2 axiom. This new version	bertot	2012-06-11
*	Adds the proof of PI_ineq, plus some other smarter ways to approximate PI	bertot	2012-06-11
*	Modifications and rearrangements to remove the action that sin (PI/2) = 1	bertot	2012-06-05
*	list_eq_dec now transparent (wish #2786)	letouzey	2012-06-01
*	Functions *_beq aren't generated anymore, remove comments about them	letouzey	2012-05-30
*	Bugs revealed by playing with contribs	pboutill	2012-05-25
*	Permutation: remove a compatibility notation which doesn't help MathClasses	letouzey	2012-05-22
*	SetoidList: explicit the fact that InfA_compat won't use ltA_strorder	letouzey	2012-05-22
*	List + Permutation : more results about nth_error and nth	letouzey	2012-05-18
*	Intuition: temporary(?) restore the unconditional unfolding of not	letouzey	2012-05-15
*	Vectors takes advantage of pattern matching compiler fixup	pboutill	2012-05-11
*	Bug 2767	pboutill	2012-05-09
*	Coqide highligthing is back (done by gtksourceview).	pboutill	2012-05-02
*	A notion of permutation for lists modulo a setoid equality	letouzey	2012-05-02
*	remove undocumented and scarcely-used tactic auto decomp	letouzey	2012-04-23
*	Remove the Dp plugin.	gmelquio	2012-04-17
*	Fixing typo in previous commit r15180.	herbelin	2012-04-15
*	Fixing tauto "special" behavior on singleton types w/ 2 parameters (bug #2680).	herbelin	2012-04-15
*	MSetRBT : implementation of MSets via Red-Black trees	letouzey	2012-04-13
*	Uniformisation in the documentation: remove the use of 'coinductive' in	aspiwack	2012-04-13
*	"A -> B" is a notation for "forall _ : A, B".	pboutill	2012-04-12
*	Fixing a few bugs (see #2571) related to interpretation of multiple binders	herbelin	2012-04-06
*	Fixing printing level of Utf8 equivalent for ->.	herbelin	2012-03-26
*	Fix interface of resolve_typeclasses: onlyargs -> with_goals:	msozeau	2012-03-20
*	Turning proofs of well-ordering of lexicographic product transparent	herbelin	2012-03-20
*	Fix bugs related to Program integration.	msozeau	2012-03-19
*	Final part of moving Program code inside the main code. Adapted add_definitio...	msozeau	2012-03-14