coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Side effect free implementation of admit (Isabelle's oracle)	gareuselesinge	2013-08-08
*	Adding a dependent version of equal_f, thus fixing #3074.	ppedrot	2013-08-02
*	Typo in definition clos_refl	ppedrot	2013-07-31
*	Fixing #3089. This implied tweaking the definition of the lexicographic	ppedrot	2013-07-26
*	Added a concat function to List theory. Strangely, it was missing.	ppedrot	2013-07-24
*	"Boolean Equality" and "Case Analysis" are already off by default...	letouzey	2013-07-17
*	More dynamic argument scopes	letouzey	2013-07-17
*	A constructive proof of Fan theorem where paths are represented by predicates.	herbelin	2013-06-02
*	Making the behavior of "injection ... as ..." more natural:	herbelin	2013-06-02
*	Improving printing of 'rew' notation	herbelin	2013-05-05
*	Relaxing the constraint on eta-expanding on the fly while looking for	herbelin	2013-05-05
*	Added group properties of eq_refl, eq_sym, eq_trans	herbelin	2013-04-17
*	Normalized type for Vector.map2	pboutill	2013-03-25
*	NMake*: avoid some warning about Let outside sections	letouzey	2013-03-22
*	Using hnf instead of "intro H" for forcing reduction to a product.	herbelin	2013-03-21
*	cbn friendly VectorDef	pboutill	2013-02-25
*	make validate repaired via a temporary fix for #2949	letouzey	2013-02-13
*	Unset Asymmetric Patterns	pboutill	2013-01-18
*	nat_iter n f x -> nat_rect _ x (fun _ => f) n	pboutill	2012-12-21
*	Rework of GenericMinMax and OrdersTac (helps extraction, cf. #2904)	letouzey	2012-12-18
*	No more constant named "int" in Coq theories (cf bug #2878)	letouzey	2012-12-18
*	Finish patch for Hint Resolve, stopping to generate new constant names for	msozeau	2012-12-08
*	Making subset_eq_compat applying over more general domain "Type" (see #2938).	herbelin	2012-12-05
*	Identities over types satisfying Uniqueness of Identity Proofs	herbelin	2012-12-04
*	Isolating the ingredients of the proof of Prop<>Type (r15973). Seeing	herbelin	2012-11-15
*	Some lemmas on property of rewriting. It will probably be worth at	herbelin	2012-11-15
*	Added a proof that Prop<>Type, for arbitrary fixed Type.	herbelin	2012-11-15
*	A decidability property of functional relations over decidable codomains.	herbelin	2012-11-15
*	For the record, two examples of short proofs of uniqueness of identity	herbelin	2012-11-15
*	Change Hint Resolve, Immediate to take a global reference as argument	msozeau	2012-10-26
*	Removed a few calls to "Opaque" in Logic.v ineffective since at least	herbelin	2012-10-24
*	Removing redundant definition of case_eq (see #2919).	herbelin	2012-10-16
*	Revert "En cours pour 'generalize in clause' et 'induction in clause'"	herbelin	2012-10-04
*	En cours pour 'generalize in clause' et 'induction in clause'	herbelin	2012-10-04
*	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