coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Merge remote-tracking branch 'gforge/v8.5' into v8.6	Matthieu Sozeau	2016-07-29
\|\
\| *	Fix #4769, univ poly and elim schemes in sections	Matthieu Sozeau	2016-07-29
* \|	primproj: warning and avoid error.	Matthieu Sozeau	2016-07-06
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-01-21
\|\\|
\| *	Update copyright headers.	Maxime Dénès	2016-01-20
* \|	Removing some goal unsafeness in inductive schemes.	Pierre-Marie Pédrot	2015-10-29
\|/
*	Avoid type checking private_constants (side_eff) again during Qed (#4357).	Enrico Tassi	2015-10-28
*	Give a way to control if the decidable-equality schemes are built like	Hugo Herbelin	2015-09-23
*	Univs: Add universe binding lists to definitions	Matthieu Sozeau	2015-09-14
*	Reverting 16 last commits, committed mistakenly using the wrong push command.	Hugo Herbelin	2015-08-02
*	Give a way to control if the decidable-equality schemes are built like	Hugo Herbelin	2015-08-02
*	Make native compiler handle universe polymorphic definitions.	Maxime Dénès	2015-01-17
*	Update headers.	Maxime Dénès	2015-01-12
*	Fix elimschemes accessing directly the universe context of inductives (fixes ...	Matthieu Sozeau	2014-08-14
*	Proofs now take and return an evar_universe_context, simplifying interfaces	Matthieu Sozeau	2014-06-18
*	Removing dead code.	Pierre-Marie Pédrot	2014-06-17
*	This commit adds full universe polymorphism and fast projections to Coq.	Matthieu Sozeau	2014-05-06
*	State Transaction Machine	gareuselesinge	2013-08-08
*	Remove some more "open" and dead code thanks to OCaml4 warnings	letouzey	2012-10-02
*	Updating headers.	herbelin	2012-08-08
*	Fixing discriminate for identity.	herbelin	2011-05-26
*	Some dead code removal, thanks to Oug analyzer	letouzey	2010-09-24
*	Updated all headers for 8.3 and trunk	herbelin	2010-07-24
*	Remove the svn-specific $Id$ annotations	letouzey	2010-04-29
*	Made the side-conditions of lemmas always come last when chaining "apply in"	herbelin	2009-12-13