coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Update headers following #6543.	Théo Zimmermann	2018-02-27
*	Ensuring all .v files end with a newline to make "sed -i" work better on them.	Hugo Herbelin	2017-08-21
*	Prelude : no more autoload of plugins extraction and recdef	Pierre Letouzey	2017-06-14
*	drop vo.itarget files and compute the corresponding the corresponding values ...	Matej Kosik	2017-06-01
*	Fix some documentation typos.	Guillaume Melquiond	2016-11-24
*	Merge branch 'v8.5' into v8.6	Pierre-Marie Pédrot	2016-10-12
\|\
\| *	Remove if_then_else. Use tryif instead.	Théo Zimmermann	2016-10-03
* \|	Giving a more natural semantics to injection by default.	Hugo Herbelin	2016-06-18
* \|	Typeclasses: stdlib fixes for new search algorithm	Matthieu Sozeau	2016-06-16
* \|	Removing "intro" from the tactic AST.	Pierre-Marie Pédrot	2016-06-03
* \|	Revert "Temporary hack to compensate missing comma while re-printing tactic"	Hugo Herbelin	2016-04-27
* \|	Temporary hack to compensate missing comma while re-printing tactic	Hugo Herbelin	2016-04-27
\|/
*	ZArith/Int.v: some modernizations	Pierre Letouzey	2015-04-02
*	MMapPositive: another implementation of MMaps	Pierre Letouzey	2015-03-06
*	Forbid Require inside interactive modules and module types.	Maxime Dénès	2014-12-25
*	Simpl less (so that cbn will not simpl too much)	Pierre Boutillier	2014-10-01
*	Keyed unification option, compiling the whole standard library	Matthieu Sozeau	2014-09-27
*	"allows to", like "allowing to", is improper	Jason Gross	2014-08-25
*	MSetRBT: unfortunate typo in compare_height (fix #3413)	Pierre Letouzey	2014-07-10
*	Arith: full integration of the "Numbers" modular framework	Pierre Letouzey	2014-07-09
*	Avoid using a deprecated lemma in the standard library.	Guillaume Melquiond	2014-06-26
*	Make standard library independent of the names generated by	Hugo Herbelin	2014-06-04
*	Making those proofs which depend on names generated for the arguments	Hugo Herbelin	2014-06-01
*	Restore implicit arguments of irreflexivity (fixes bug #3305).	Matthieu Sozeau	2014-05-09
*	Try a new way of handling template universe levels	Matthieu Sozeau	2014-05-06
*	- Fix arity handling in retyping (de Bruijn bug!)	Matthieu Sozeau	2014-05-06
*	- Fix bug preventing apply from unfolding Fixpoints.	Matthieu Sozeau	2014-05-06
*	Correct rebase on STM code. Thanks to E. Tassi for help on dealing with	Matthieu Sozeau	2014-05-06
*	This commit adds full universe polymorphism and fast projections to Coq.	Matthieu Sozeau	2014-05-06
*	Cbn is happier when ?SetPositive fixpoints have the set as recursive argument	Pierre Boutillier	2014-05-02
*	Eta contractions to please cbn	Pierre Boutillier	2014-05-02
*	"Boolean Equality" and "Case Analysis" are already off by default...	letouzey	2013-07-17
*	No more constant named "int" in Coq theories (cf bug #2878)	letouzey	2012-12-18
*	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
*	MSetRBT: a tail-recursive plength	letouzey	2012-08-06
*	induction/destruct : nicer syntax for generating equations (solves #2741)	letouzey	2012-07-09
*	MSetRBT : elementary arith proofs instead of calls to lia	letouzey	2012-07-05
*	ZArith + other : favor the use of modern names instead of compat notations	letouzey	2012-07-05
*	MSetRBT : implementation of MSets via Red-Black trees	letouzey	2012-04-13
*	MSetAVL: better implementation of filter suggested by X. Leroy	letouzey	2012-01-17
*	theories/, plugins/ and test-suite/ ported to the Arguments vernacular	gareuselesinge	2011-11-21
*	MSet/FSet/FMap : add more explicitly an alternative spec for fold via fold_right	letouzey	2011-10-14
*	fsetdec : non-atomic elements are now transformed as variables first (fix #2464)	letouzey	2011-10-07
*	Improved handling of element equalities in fsetdec (fix #2467)	letouzey	2011-10-07
*	Modularization of BinInt, related fixes in the stdlib	letouzey	2011-05-05
*	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
*	- Use transparency information all the way through unification and	msozeau	2011-02-17
*	s/appartness/membership/g (Closes: #2470)	glondu	2011-01-06