coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-09-14
\|\
\| *	Merge branch 'v8.5' into v8.6	Pierre-Marie Pédrot	2016-09-14
\|/\|
\| *	Fixing #5077 (failure on typing a fixpoint with evars in its type).	Hugo Herbelin	2016-09-10
* \|	Make it a bit more obvious when variables are of type unit.	Guillaume Melquiond	2016-08-10
* \|	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
* \| \|	Splitting Evarutil in two distinct files.	Pierre-Marie Pédrot	2016-03-20
* \| \|	merging conflicts with the original "trunk__CLEANUP__Context__2" branch	Matej Kosik	2016-02-15
\|\ \ \
* \| \| \|	Renaming functions in Typing to stick to the standard e_* scheme.	Pierre-Marie Pédrot	2016-02-15
\| * \| \|	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
* \| \|	Merge branch 'v8.5' into trunk	Guillaume Melquiond	2015-12-31
\|\\| \|
\| * \|	(Partial) fix for bug #4453: raise an error instead of an anomaly.	Matthieu Sozeau	2015-12-17
* \| \|	Fixing unexpected length of context in a typing function, detected by	Hugo Herbelin	2015-12-15
* \| \|	Unifying betazeta_applist and prod_applist into a clearer interface.	Hugo Herbelin	2015-12-05
\|/ /
\| *	Add a flag to deactivate guard checking in the kernel.	Arnaud Spiwack	2015-06-26
\|/
*	Safer typing primitives.	Pierre-Marie Pédrot	2015-05-13
*	Update headers.	Maxime Dénès	2015-01-12
*	Fixing a bug in the presence of let-in in inductive arity.	Hugo Herbelin	2014-10-20
*	Providing a -type-in-type option for collapsing the universe hierarchy.	Hugo Herbelin	2014-09-13
*	Proofview refiner is now type-safe by default.	Pierre-Marie Pédrot	2014-09-04
*	Typing.sort_of does not leak evarmaps anymore.	Pierre-Marie Pédrot	2014-09-04
*	A tentative uniform naming policy in module Inductiveops.	Hugo Herbelin	2014-08-01
*	Quickly fixing bug #2996: typing functions now check when referring to	Hugo Herbelin	2014-06-28
*	Change interface of refresh universes to get a pbty argument instead of	Matthieu Sozeau	2014-06-26
*	- Add an option to refresh only algebraic universes, for e_type_of. The goal	Matthieu Sozeau	2014-06-21
*	Cleanup treatment of template universe polymorphism (thanks to E. Tassi	Matthieu Sozeau	2014-06-20
*	Refresh universes for Ltac's type_of, as the term can be used anywhere,	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
*	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
*	Remove many superfluous 'open' indicated by ocamlc -w +33	Pierre Letouzey	2014-03-05
*	More monomorphic List.mem + List.assoc + ...	letouzey	2013-10-24
*	Delayed the computation of parameters in sort polymorphism of	herbelin	2013-05-14
*	Splitting Term into five unrelated interfaces:	ppedrot	2013-04-29
*	A more informative message when the elimination predicate for	herbelin	2013-02-17
*	Moved code from Pretype_error to Evarutil	ppedrot	2013-02-10
*	Uniformization of the "anomaly" command.	ppedrot	2013-01-28
*	Taking into account the possibility of having a type of type which is	herbelin	2012-12-18
*	Monomorphization (pretyping)	ppedrot	2012-11-22
*	Moving Utils.list_* to a proper CList module, which includes stdlib	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