coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...	Pierre Letouzey	2016-07-03
*	Separate flags for fix/cofix/match reduction and clean reduction function names.	Maxime Dénès	2016-07-01
*	Moving the typing_flags to the environment.	Pierre-Marie Pédrot	2016-06-18
*	Factorizing the uses of Declareops.safe_flags.	Pierre-Marie Pédrot	2016-06-16
*	Merge PR #79: Let the kernel assume that a (co-)inductive type is positive.	Pierre-Marie Pédrot	2016-06-16
\|\
\| *	Assume totality: dedicated type rather than bool	Arnaud Spiwack	2016-06-14
* \|	Renaming variants of Entries.local_entry	Matej Kosik	2016-02-16
* \|	CLEANUP: Context.{Rel,Named}.Declaration.t	Matej Kosik	2016-02-09
* \|	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
\|/ /
* \|	Miscellaneous typos, spacing, US spelling in comments or variable names.	Hugo Herbelin	2015-10-18
* \|	Fix #4346 2/2: VM casts were not inferring universe constraints.	Maxime Dénès	2015-10-15
* \|	Fix #4346 1/2: native casts were not inferring universe constraints.	Maxime Dénès	2015-10-15
* \|	Univs: be more restrictive for template polymorphic constants: only	Matthieu Sozeau	2015-10-12
* \|	Option -type-in-type: added support in checker and making it contaminating	Hugo Herbelin	2015-07-10
\| *	Add a flag to deactivate guard checking in the kernel.	Arnaud Spiwack	2015-06-26
\|/
*	Fix typeops ignoring results of check functions with let _, and one	Matthieu Sozeau	2015-02-10
*	Update headers.	Maxime Dénès	2015-01-12
*	Add a boolean to indicate the unfolding state of a primitive projection,	Matthieu Sozeau	2014-09-27
*	Change the way primitive projections are declared to the kernel.	Matthieu Sozeau	2014-08-28
*	Move to a representation of universe polymorphic constants using indices for ...	Matthieu Sozeau	2014-08-03
*	Quickly fixing bug #2996: typing functions now check when referring to	Hugo Herbelin	2014-06-28
*	- Fix hashing of levels to get the "right" order in universe contexts etc...	Matthieu Sozeau	2014-06-04
*	Reuse universe level substitutions for template polymorphism, fixing performance	Matthieu Sozeau	2014-05-09
*	- Fix bug preventing apply from unfolding Fixpoints.	Matthieu Sozeau	2014-05-06
*	Fix interface for template polymorphism, cleaning up code in all typing algor...	Matthieu Sozeau	2014-05-06
*	Properly reinstate old-style polymorphism in the kernel and pretyping/retyping.	Matthieu Sozeau	2014-05-06
*	Initial work on reintroducing old-style polymorphism for compatibility (the s...	Matthieu Sozeau	2014-05-06
*	This commit adds full universe polymorphism and fast projections to Coq.	Matthieu Sozeau	2014-05-06
*	Useless Array.to_list in Typeops.	Pierre-Marie Pédrot	2014-03-10
*	Support for evars and metas in native compiler.	Maxime Dénès	2013-12-30
*	Delayed the computation of parameters in sort polymorphism of	herbelin	2013-05-14
*	Merging Context and Sign.	ppedrot	2013-04-29
*	Splitting Term into five unrelated interfaces:	ppedrot	2013-04-29
*	More informative error when a global reference is used in a context of	herbelin	2013-02-28
*	Uniformization of the "anomaly" command.	ppedrot	2013-01-28
*	New implementation of the conversion test, using normalization by evaluation to	mdenes	2013-01-22
*	Monomorphization (kernel)	ppedrot	2012-11-22
*	As r15801: putting everything from Util.array_* to CArray.*.	ppedrot	2012-09-14
*	This patch removes unused "open" (automatically generated from	regisgia	2012-09-14
*	The new ocaml compiler (4.00) has a lot of very cool warnings,	regisgia	2012-09-14
*	Updating headers.	herbelin	2012-08-08
*	Noise for nothing	pboutill	2012-03-02
*	Completing r14448 and thus continuing r14407 (using Cast to propagate	herbelin	2011-09-24
*	Having added a special Cast for remembering the use of conversion	herbelin	2011-09-04
*	Propagated information from the reduction tactics to the kernel so	herbelin	2011-08-10
*	Term_typing, Typeops: replace some generic '=' on constr by eq_constr	puech	2011-07-29
*	Revert "Add [Polymorphic] flag for defs"	msozeau	2011-04-13
*	Add [Polymorphic] flag for defs	msozeau	2011-04-13