coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	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
* \|	Merge branch 'v8.5' into v8.6	Pierre-Marie Pédrot	2016-07-07
\|\\|
\| *	Move option_map notation up	Jason Gross	2016-07-05
\| *	Restore option_map in FMapFacts	Jason Gross	2016-07-05
* \|	Giving a more natural semantics to injection by default.	Hugo Herbelin	2016-06-18
\|/
*	Fix some typos.	Guillaume Melquiond	2015-12-07
*	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
*	- Fix printing and parsing of primitive projections, including the Set	Matthieu Sozeau	2014-09-09
*	instanciation is French, instantiation is English	Jason Gross	2014-08-25
*	Grammar: "allowing to" is not proper English	Jason Gross	2014-08-25
*	More proofs independent of the names generated by induction/elim over	Hugo Herbelin	2014-08-05
*	Adding a generalized version of fold_Equal to FMapFacts.	Pierre Courtieu	2014-07-31
*	Avoid using a deprecated lemma in the standard library.	Guillaume Melquiond	2014-06-26
*	Cleanup treatment of template universe polymorphism (thanks to E. Tassi	Matthieu Sozeau	2014-06-20
*	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
*	Fix after merge.	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
*	Unset Asymmetric Patterns	pboutill	2013-01-18
*	No more constant named "int" in Coq theories (cf bug #2878)	letouzey	2012-12-18
*	Ltac repeat is in fact already doing progress	letouzey	2012-10-01
*	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
*	Intuition: temporary(?) restore the unconditional unfolding of not	letouzey	2012-05-15
*	Fixing tauto "special" behavior on singleton types w/ 2 parameters (bug #2680).	herbelin	2012-04-15
*	Final part of moving Program code inside the main code. Adapted add_definitio...	msozeau	2012-03-14
*	Revert "Tentative to fix bug #2628 by not letting intuition break records. Mi...	msozeau	2012-01-31
*	Tentative to fix bug #2628 by not letting intuition break records. Might be t...	msozeau	2012-01-28
*	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
*	- 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
*	Fix compilation issues.	msozeau	2011-02-16
*	- Fix treatment of globality flag for typeclass instance hints (they	msozeau	2011-02-14
*	s/appartness/membership/g (Closes: #2470)	glondu	2011-01-06
*	Cosmetic : let's take advantage of the n-ary exists notation	letouzey	2010-12-17
*	FMapFacts: typo noticed by Aaron	letouzey	2010-10-22
*	Extraction: re-introduce some eta-expansions in rare situations leading to '_...	letouzey	2010-09-20
*	For the moment, two small manual eta-expansions to avoid '_a after extraction	letouzey	2010-09-17