coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Swapping Context and Constr: defining declarations on constr in Constr.	Hugo Herbelin	2018-06-27
*	Remove reference name type.	Maxime Dénès	2018-06-18
*	Merge PR #7419: Remove 100 occurrences of Evd.empty	Pierre-Marie Pédrot	2018-05-28
\|\
\| *	Remove some occurrences of Evd.empty	Maxime Dénès	2018-05-25
* \|	Remove the unused printer_pr mechanism.	Jim Fehrle	2018-05-24
\|/
*	Split off Universes functions dealing with names.	Gaëtan Gilbert	2018-05-17
*	Evar maps contain econstrs.	Gaëtan Gilbert	2018-04-13
*	[located] Push inner locations in `reference` to a CAst.t node.	Emilio Jesus Gallego Arias	2018-03-09
*	Merge PR #6816: Adding mention of shelved/given-up status in Show Existentials	Maxime Dénès	2018-03-08
\|\
* \|	Update headers following #6543.	Théo Zimmermann	2018-02-27
\| *	Adding mention of shelved/given-up status in "Show Existentials".	Hugo Herbelin	2018-02-22
\|/
*	Print inductive cumulativity info in About.	Gaëtan Gilbert	2018-02-11
*	[proof] Embed evar_map in RefinerError exception.	Emilio Jesus Gallego Arias	2017-12-11
*	Merge PR #1033: Universe binder improvements	Maxime Dénès	2017-11-28
\|\
* \|	[api] Remove aliases of `Evar.t`	Emilio Jesus Gallego Arias	2017-11-26
\| *	When declaring constants/inductives use ContextSet if monomorphic.	Gaëtan Gilbert	2017-11-24
\| *	Separate checking univ_decls and obtaining universe binder names.	Gaëtan Gilbert	2017-11-24
\|/
*	[api] Deprecate Term destructors, move to Constr	Emilio Jesus Gallego Arias	2017-11-22
*	[printing] Deprecate all printing functions accessing the global proof.	Emilio Jesus Gallego Arias	2017-11-21
*	[proof] Attempt to deprecate some V82 parts of the proof API.	Emilio Jesus Gallego Arias	2017-11-19
*	[api] Another large deprecation, `Nameops`	Emilio Jesus Gallego Arias	2017-11-13
*	[api] Move structures deprecated in the API to the core.	Emilio Jesus Gallego Arias	2017-11-06
*	[api] Deprecate all legacy uses of Names in core.	Emilio Jesus Gallego Arias	2017-11-06
*	Finish removing Show Goal uid	Gaëtan Gilbert	2017-11-04
*	Exporting the level-parametric printer of constr and its variants.	Hugo Herbelin	2017-11-02
*	Merge PR #830: Moving assert (the "Cut" rule) to new proof engine	Maxime Dénès	2017-08-29
\|\
* \|	Printing goals does not evar-normalizes beforehand anymore.	Pierre-Marie Pédrot	2017-08-01
* \|	Detyping functions are now operating on EConstr.t.	Pierre-Marie Pédrot	2017-08-01
* \|	Merge PR #919: Remove a few useless evar-normalizations in printing code.	Maxime Dénès	2017-08-01
\|\ \
* \| \|	deprecate Pp.std_ppcmds type alias	Matej Košík	2017-07-27
\| * \|	Remove a few useless evar-normalizations in printing code.	Pierre-Marie Pédrot	2017-07-26
\|/ /
* \|	Merge PR #770: [proof] Move bullets to their own module.	Maxime Dénès	2017-07-19
\|\ \
* \| \|	Bump year in headers.	Pierre-Marie Pédrot	2017-07-04
\| \| *	Moving "assert" (internally "Cut") to the new proof engine.	Hugo Herbelin	2017-06-25
\| \|/ \|/\|
* \|	Clean up universes of constants and inductives	Amin Timany	2017-06-16
* \|	Add printing of cumulativity in inductive types	Amin Timany	2017-06-16
* \|	Using UInfoInd for universes in inductive types	Amin Timany	2017-06-16
\| *	[proof] Move bullets to their own module.	Emilio Jesus Gallego Arias	2017-06-12
* \|	[proof] Deprecate redundant wrappers.	Emilio Jesus Gallego Arias	2017-06-11
\|/
*	[emacs] [toplevel] Make emacs flag local to the toplevel.	Emilio Jesus Gallego Arias	2017-06-01
*	[cleanup] Unify all calls to the error function.	Emilio Jesus Gallego Arias	2017-05-27
*	Merge PR#481: [option] Remove support for non-synchronous options.	Maxime Dénès	2017-05-25
\|\
* \	Merge branch 'trunk' into located_switch	Emilio Jesus Gallego Arias	2017-05-24
\|\ \
\| \| *	[option] Remove support for non-synchronous options.	Emilio Jesus Gallego Arias	2017-05-24
\| \|/
\| *	Merge PR#457: Adding an even more compact goal hyps mode.	Maxime Dénès	2017-05-17
\| \|\
\| \| *	Simplified compaction criterion + tests.	Pierre Courtieu	2017-05-16
\| \| *	Adapted to EConstr.	Pierre Courtieu	2017-05-05
\| * \|	Warning removed.	Pierre Courtieu	2017-05-04
\| * \|	labelizing arguments	Pierre Courtieu	2017-05-04
\| * \|	Adding an option "Printing Unfocused".	Pierre Courtieu	2017-05-04