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
*	Feedback cleanup	Emilio Jesus Gallego Arias	2016-05-31
*	Removing dead code and unused opens.	Pierre-Marie Pédrot	2016-05-08
*	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-04-09
\|\
\| *	Fixing a source of inefficiency and an artificial dependency in the	Daniel de Rauglaudre	2016-04-08
* \|	CLEANUP: Context.{Rel,Named}.Declaration.t	Matej Kosik	2016-02-09
\|/
*	Update copyright headers.	Maxime Dénès	2016-01-20
*	Univs: fix an evar leak in congruence	Matthieu Sozeau	2015-10-02
*	Safer typing primitives.	Pierre-Marie Pédrot	2015-05-13
*	Update headers.	Maxime Dénès	2015-01-12
*	fix bug #2447 in congruence	Pierre Corbineau	2014-12-16
*	Add a boolean to indicate the unfolding state of a primitive projection,	Matthieu Sozeau	2014-09-27
*	Adding a new Control file centralizing the control options of Coq.	Pierre-Marie Pédrot	2014-06-07
*	This commit adds full universe polymorphism and fast projections to Coq.	Matthieu Sozeau	2014-05-06
*	Getting rid of generic hashes in cc plugin.	Pierre-Marie Pédrot	2014-03-03
*	Fixing pervasive comparisons	Pierre-Marie Pédrot	2014-03-01
*	Avoid polymorphic comparison (plugins/cc).	xclerc	2013-10-14
*	Removing a bunch of generic equalities.	ppedrot	2013-09-27
*	Added a more efficient way to recover the domain of a map.	ppedrot	2013-08-25
*	Tentative fix for #3054: we refresh universes in a term generated	ppedrot	2013-07-29
*	Splitting Term into five unrelated interfaces:	ppedrot	2013-04-29
*	Restrict (try...with...) to avoid catching critical exn (part 9)	letouzey	2013-03-13
*	Fixed synchronicity of filter with evar context in new_goal_with.	herbelin	2013-01-29
*	Uniformization of the "anomaly" command.	ppedrot	2013-01-28
*	Array.create is deprecated	pboutill	2012-12-19
*	Modulification of identifier	ppedrot	2012-12-14
*	Moved Intset and Intmap to Int namespace.	ppedrot	2012-12-14
*	Remove some more "open" and dead code thanks to OCaml4 warnings	letouzey	2012-10-02
*	Cleaning, renaming obscure functions and documenting in Hashcons.	ppedrot	2012-09-26
*	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
*	Getting rid of Pp.msgnl and Pp.message.	ppedrot	2012-06-01
*	Getting rid of Pp.msg	ppedrot	2012-05-30
*	Noise for nothing	pboutill	2012-03-02
*	Added a DEPRECATED flag in declaration of options. For now only two options a...	ppedrot	2011-11-24
*	Ccalgo, Ccproof: multiple generic Hashtbl on constr and term replaced by Cons...	puech	2011-07-29
*	Ccproof: generic equality on term replaced by term_equal	puech	2011-07-29
*	commit 13400 and 13409.	soubiran	2010-09-13
*	Updated all headers for 8.3 and trunk	herbelin	2010-07-24
*	Remove the svn-specific $Id$ annotations	letouzey	2010-04-29
*	Here comes the commit, announced long ago, of the new tactic engine.	aspiwack	2010-04-22
*	Delete trailing whitespaces in all .{v,ml} files	glondu	2009-09-17
*	Improved parameterization of Coq:	herbelin	2009-08-02
*	Directory 'contrib' renamed into 'plugins', to end confusion with archive of ...	letouzey	2009-03-20