coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Merge PR #6855: Update headers following #6543.	Maxime Dénès	2018-03-05
\|\
* \|	Turn warning for deprecated notations on.	Théo Zimmermann	2018-03-02
* \|	Remove the deprecation for some 8.2-8.5 compatibility aliases.	Théo Zimmermann	2018-03-02
\| *	Update headers following #6543.	Théo Zimmermann	2018-02-27
\|/
*	Fix warning about shadowing a global name.	Gaëtan Gilbert	2017-12-19
*	[ltac] Warning for deprecated `Add Setoid` and `Add Morphism` forms.	Emilio Jesus Gallego Arias	2017-10-05
*	Ensuring all .v files end with a newline to make "sed -i" work better on them.	Hugo Herbelin	2017-08-21
*	Removing a dummy parameter in some FMapPositive statements.	Hugo Herbelin	2017-07-16
*	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
* \|	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