coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Returning instance instead of substitution in universe context abstraction.	Pierre-Marie Pédrot	2017-12-30
*	[api] Move structures deprecated in the API to the core.	Emilio Jesus Gallego Arias	2017-11-06
*	[stm] Remove state-handling from Futures.	Emilio Jesus Gallego Arias	2017-10-17
*	Bump year in headers.	Pierre-Marie Pédrot	2017-07-04
*	Clean up universes of constants and inductives	Amin Timany	2017-06-16
*	Drop '.' from CErrors.anomaly, insert it in args	Jason Gross	2017-06-02
*	[cleanup] Unify all calls to the error function.	Emilio Jesus Gallego Arias	2017-05-27
*	Adding the size of the opaquetab in its representation.	Pierre-Marie Pédrot	2017-03-27
*	Fix hashconsing of terms in the kernel.	Pierre-Marie Pédrot	2017-03-27
*	[future] Remove unused parameter greedy.	Emilio Jesus Gallego Arias	2017-03-14
*	errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...	Pierre Letouzey	2016-07-03
*	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-01-21
\|\
\| *	Update copyright headers.	Maxime Dénès	2016-01-20
* \|	CLEANUP: kernel/context.ml{,i}	Matej Kosik	2016-01-11
\|/
*	Avoid type checking private_constants (side_eff) again during Qed (#4357).	Enrico Tassi	2015-10-28
*	Update headers.	Maxime Dénès	2015-01-12
*	library/opaqueTables: enable their use in interactive mode	Enrico Tassi	2014-10-13
*	Move to a representation of universe polymorphic constants using indices for ...	Matthieu Sozeau	2014-08-03
*	- Fix bug preventing apply from unfolding Fixpoints.	Matthieu Sozeau	2014-05-06
*	Adapt universe polymorphic branch to new handling of futures for delayed proofs.	Matthieu Sozeau	2014-05-06
*	This commit adds full universe polymorphism and fast projections to Coq.	Matthieu Sozeau	2014-05-06
*	Opaqueproofs: sink futures when interactive	Enrico Tassi	2014-04-25
*	Lazyconstr -> Opaqueproof	Enrico Tassi	2014-02-26