coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
\| * \|	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
*	Noise for nothing	pboutill	2012-03-02
*	Renamig support added to "Arguments"	gareuselesinge	2011-11-21
*	Still more unification in typing.ml	herbelin	2011-10-25
*	More unification in type_of and addition of e_type_of to get the new	herbelin	2011-10-24
*	Unification in the return clause of match was not supported in solve_evars.	herbelin	2011-10-11
*	Applied the trick of Chung-Kil Hur to solve second-order matching	herbelin	2011-10-10
*	It happens that the type inference algorithm (pretyping) did not check	herbelin	2011-10-05
*	Replaced printing number of ill-typed branch by printing name of constructor	herbelin	2011-04-08
*	Some dead code removal, thanks to Oug analyzer	letouzey	2010-09-24