coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Remove unused env argument to fresh_sort_in_family	Gaëtan Gilbert	2018-07-03
*	Deprecate mixing univ minimization and evm normalization functions.	Gaëtan Gilbert	2018-04-17
*	Update headers following #6543.	Théo Zimmermann	2018-02-27
*	[api] Move structures deprecated in the API to the core.	Emilio Jesus Gallego Arias	2017-11-06
*	Getting rid of AUContext abstraction breakers in Elimschemes.	Pierre-Marie Pédrot	2017-07-13
*	Safe API for accessing universe constraints of global references.	Pierre-Marie Pédrot	2017-07-11
*	Bump year in headers.	Pierre-Marie Pédrot	2017-07-04
*	Clean up universes of constants and inductives	Amin Timany	2017-06-16
*	Squashed commit of the following:	Amin Timany	2017-06-16
*	Remove the Sigma (monotonous state) API.	Maxime Dénès	2017-06-06
*	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