coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
*	More dynamic argument scopes	letouzey	2013-07-17
*	NMake*: avoid some warning about Let outside sections	letouzey	2013-03-22
*	make validate repaired via a temporary fix for #2949	letouzey	2013-02-13
*	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
*	Finish patch for Hint Resolve, stopping to generate new constant names for	msozeau	2012-12-08
*	Change Hint Resolve, Immediate to take a global reference as argument	msozeau	2012-10-26
*	Ltac repeat is in fact already doing progress	letouzey	2012-10-01
*	fast bitwise operations (lor,land,lxor) on int31 and BigN	letouzey	2012-08-11
*	Updating headers.	herbelin	2012-08-08
*	induction/destruct : nicer syntax for generating equations (solves #2741)	letouzey	2012-07-09
*	ZArith + other : favor the use of modern names instead of compat notations	letouzey	2012-07-05
*	Granted legitimate wish #2607 (not exposing crude fixpoint body of	herbelin	2011-12-18
*	theories/, plugins/ and test-suite/ ported to the Arguments vernacular	gareuselesinge	2011-11-21
*	Merge subinstances branch by me and Tom Prince.	msozeau	2011-11-17
*	Give inner fixpoint of gcd31 a name, to avoid excessive unfolding	glondu	2011-08-17
*	SearchAbout and similar: add a customizable blacklist	letouzey	2011-08-11
*	Cleanup of files related with power over Z.	letouzey	2011-07-01
*	Cleanup in SpecViaZ	letouzey	2011-06-30
*	Cleanup of Ndigits	letouzey	2011-06-30
*	Deletion of useless Zdigits_def	letouzey	2011-06-28
*	Deletion of useless Zlog_def	letouzey	2011-06-28
*	Deletion of useless Zsqrt_def	letouzey	2011-06-28
*	Some cleanup of Zdiv and Zquot, deletion of useless Zdiv_def	letouzey	2011-06-28
*	Clean-up of Znumtheory, deletion of Zgcd_def	letouzey	2011-06-24
*	Numbers: a particular case of div_unique	letouzey	2011-06-24
*	Numbers: change definition of divide (compat with Znumtheory)	letouzey	2011-06-24
*	Some more cleanup of Zorder	letouzey	2011-06-23
*	Some migration of results from BinInt to Numbers	letouzey	2011-06-20
*	Zcompare.destr_zcompare subsumed by case Z.compare_spec	letouzey	2011-06-20
*	Arithemtic: more concerning compare, eqb, leb, ltb	letouzey	2011-06-20
*	Some simplifications in NZDomain	letouzey	2011-06-20
*	Modularization of BinInt, related fixes in the stdlib	letouzey	2011-05-05
*	Modularization of BinNat + fixes of stdlib	letouzey	2011-05-05
*	Modularization of BinPos + fixes in Stdlib	letouzey	2011-05-05
*	Definitions of positive, N, Z moved in Numbers/BinNums.v	letouzey	2011-05-05
*	Fix generated script for NMake, a rewrite necessitates full conversion for	msozeau	2011-04-18
*	Cyclic: a small optimisation with nice effect on BigN.mul (thinks Benjamin)	letouzey	2011-03-30
*	CompareSpec: a slight generalization/reformulation of CompSpec	letouzey	2011-03-17
*	- Add modulo_delta_types flag for unification to allow full	msozeau	2011-03-13
*	ZBits,ZdivEucl,ZDivFloor: a few lemmas with weaker preconditions	letouzey	2011-03-10
*	BigQ : setting correct arguments scopes	letouzey	2011-02-23
*	- Use transparency information all the way through unification and	msozeau	2011-02-17
*	An automatic substitution of scope at functor application	letouzey	2011-02-11
*	Annotations at functor applications:	letouzey	2011-02-11
*	A fine-grain control of inlining at functor application via priority levels	letouzey	2011-01-31
*	Remove the "Boxed" syntaxes and the const_entry_boxed field	letouzey	2011-01-28
*	Numbers: simplier spec for testbit	letouzey	2011-01-20
*	Ndigits: a Pshiftl_nat used in BigN (was double_digits there)	letouzey	2011-01-04
*	f_equiv : a clone of f_equal that handles setoid equivalences	letouzey	2011-01-04