coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	List: Bug 3039 weaker requirement for fold symmetric	Pierre Boutillier	2013-12-20
*	Better unification for [projT1] and [proj1_sig].	Jason Gross	2013-12-12
*	Generalize eq_proofs_unicity	Jason Gross	2013-12-12
*	Improved the presentation of the proof of UIP_refl_nat.	Hugo Herbelin	2013-12-04
*	Add lemma derivable_pt_lim_atan.	Guillaume Melquiond	2013-12-04
*	Fix statement of Rplus_lt_reg_r and add Rplus_lt_reg_l.	Guillaume Melquiond	2013-12-03
*	Remove a useless hypothesis from Rle_Rinv.	Guillaume Melquiond	2013-12-03
*	Adding Acc_intro_generator in order to help computations of Function in parti...	forest	2013-11-20
*	Nicer infered names in refine.	aspiwack	2013-11-04
*	Restore Zsqrt compat now that refine works fine with match.	aspiwack	2013-11-02
*	A whole new implemenation of the refine tactic.	aspiwack	2013-11-02
*	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