coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Remove Sorts.contents	Gaëtan Gilbert	2018-06-26
*	Collecting Array.smart_* functions into a module Array.Smart.	Hugo Herbelin	2018-05-23
*	Congruence: Fixing a bug with native projections.	Hugo Herbelin	2018-03-27
*	Congruence: typography in a comment.	Hugo Herbelin	2018-03-27
*	Congruence: getting rid of a detour by the compatibility layer of proof engine.	Hugo Herbelin	2018-03-27
*	Update headers following #6543.	Théo Zimmermann	2018-02-27
*	[api] Deprecate Term destructors, move to Constr	Emilio Jesus Gallego Arias	2017-11-22
*	[api] Move structures deprecated in the API to the core.	Emilio Jesus Gallego Arias	2017-11-06
*	[API] Remove `open API` in ml files in favor of `-open API` flag.	Emilio Jesus Gallego Arias	2017-07-17
*	Bump year in headers.	Pierre-Marie Pédrot	2017-07-04
*	Removing Proof_type from the API.	Pierre-Marie Pédrot	2017-06-16
*	Remove (useless) aliases from the API.	Matej Košík	2017-06-10
*	Put all plugins behind an "API".	Matej Kosik	2017-06-07
*	Drop '.' from CErrors.anomaly, insert it in args	Jason Gross	2017-06-02
*	[option] Remove support for non-synchronous options.	Emilio Jesus Gallego Arias	2017-05-24
*	Merge branch 'master'.	Pierre-Marie Pédrot	2017-02-14
\|\
* \|	Removing various compatibility layers of tactics.	Pierre-Marie Pédrot	2017-02-14
* \|	Ltac now uses evar-based constrs.	Pierre-Marie Pédrot	2017-02-14
* \|	Tacmach API using EConstr.	Pierre-Marie Pédrot	2017-02-14
\| *	Extend Fast_typeops to be a replacement for Typeops	Gaetan Gilbert	2016-12-12
\|/
*	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