coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Use Entries.constant_universes_entry more.	Gaëtan Gilbert	2017-11-24
*	When declaring constants/inductives use ContextSet if monomorphic.	Gaëtan Gilbert	2017-11-24
*	Fix defining non primitive projections with abstracted universes.	Gaëtan Gilbert	2017-11-24
*	Register universe binders for record projections.	Gaëtan Gilbert	2017-11-24
*	Stop exposing UState.universe_context and its Evd wrapper.	Gaëtan Gilbert	2017-11-24
*	Separate checking univ_decls and obtaining universe binder names.	Gaëtan Gilbert	2017-11-24
*	Use Maps and ids for universe binders	Gaëtan Gilbert	2017-11-24
*	Merge PR #6197: [plugin] Remove LocalityFixme über hack.	Maxime Dénès	2017-11-24
\|\
* \	Merge PR #6203: Fix universe polymorphic Program obligations.	Maxime Dénès	2017-11-23
\|\ \
\| \| *	[plugin] Remove LocalityFixme über hack.	Emilio Jesus Gallego Arias	2017-11-22
\| \| *	[plugin] Encapsulate modifiers to vernac commands.	Emilio Jesus Gallego Arias	2017-11-22
* \| \|	[api] Deprecate Term destructors, move to Constr	Emilio Jesus Gallego Arias	2017-11-22
\| * \|	Fix universe polymorphic Program obligations.	Matthieu Sozeau	2017-11-22
* \| \|	[api] Miscellaneous consolidation + moves to engine.	Emilio Jesus Gallego Arias	2017-11-21
\| \|/ \|/\|
* \|	[printing] Deprecate all printing functions accessing the global proof.	Emilio Jesus Gallego Arias	2017-11-21
* \|	Merge PR #6185: [parser] Remove unnecessary statically initialized hook.	Maxime Dénès	2017-11-21
\|\ \
* \ \	Merge PR #6181: [proof] Attempt to deprecate some V82 parts of the proof API.	Maxime Dénès	2017-11-21
\|\ \ \ \| \|_\|/ \|/\| \|
* \| \|	Merge PR #6183: [plugins] Prepare plugin API for functional handling of state.	Maxime Dénès	2017-11-20
\|\ \ \
* \ \ \	Merge PR #6125: Fixing remaining problems with bug #5762 and PR #1120 (clause...	Maxime Dénès	2017-11-20
\|\ \ \ \
\| \| \| \| *	[parser] Remove unnecessary statically initialized hook.	Emilio Jesus Gallego Arias	2017-11-19
\| \|_\|_\|/ \|/\| \| \|
\| \| * \|	[plugins] Prepare plugin API for functional handling of state.	Emilio Jesus Gallego Arias	2017-11-19
\| \| * \|	[vernac] Increase table size.	Emilio Jesus Gallego Arias	2017-11-19
\| \|/ / \|/\| \|
\| \| *	[proof] Attempt to deprecate some V82 parts of the proof API.	Emilio Jesus Gallego Arias	2017-11-19
\| \|/ \|/\|
* \|	Merge PR #6148: [api] Another large deprecation, `Nameops` and friends.	Maxime Dénès	2017-11-16
\|\ \
* \| \|	Fixes #6129 (declaration of coercions made compatible with local definitions).	Hugo Herbelin	2017-11-14
\| * \|	[api] Insert miscellaneous API deprecation back to core.	Emilio Jesus Gallego Arias	2017-11-13
\| * \|	[api] Another large deprecation, `Nameops`	Emilio Jesus Gallego Arias	2017-11-13
\|/ /
\| *	Fixing a remaining "coqdoc" problem with bug #5762 and pr #1120.	Hugo Herbelin	2017-11-08
* \|	[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
\|/
*	Merge PR #6064: [api] Deprecate all legacy uses of Name.Id in core.	Maxime Dénès	2017-11-06
\|\
* \	Merge PR #6063: Finish removing Show Goal uid	Maxime Dénès	2017-11-06
\|\ \
\| \| *	[api] Deprecate all legacy uses of Name.Id in core.	Emilio Jesus Gallego Arias	2017-11-04
\| * \|	Finish removing Show Goal uid	Gaëtan Gilbert	2017-11-04
\| \|/
* /	provide "loc : Loc.t" binding within "VERNAC COMMAND EXTEND" rules	Matej Košík	2017-11-01
\|/
*	Merge PR #677: Trunk+abstracting injection flags	Maxime Dénès	2017-10-27
\|\
\| *	Passing around the flag for injection so that tactics calling inj at	Hugo Herbelin	2017-10-26
* \|	Removing dead code which raised questions.	Hugo Herbelin	2017-10-24
\|/
*	Merge PR #1120: Fixing BZ#5762 (supporting implicit arguments in "where" clau...	Maxime Dénès	2017-10-20
\|\
* \|	[vernac] [state] Cache freeze/unfreeze	Emilio Jesus Gallego Arias	2017-10-17
* \|	[stm] Remove state-handling from Futures.	Emilio Jesus Gallego Arias	2017-10-17
* \|	[stm] Move interpretation state to Vernacentries	Emilio Jesus Gallego Arias	2017-10-17
* \|	Parse [Proof using Type] without translating Type to an id.	Gaëtan Gilbert	2017-10-10
* \|	Use a nice printer for constant names in Suggest Proof Using.	Gaëtan Gilbert	2017-10-10
* \|	Code factorization Vernacentries.interp on VernacProof.	Gaëtan Gilbert	2017-10-10
* \|	[vernac] Remove "Proof using" hacks from parser.	Emilio Jesus Gallego Arias	2017-10-10
* \|	Take Suggest Proof Using outside the kernel.	Gaëtan Gilbert	2017-10-10
* \|	Merge PR #1053: [deps] Move `Discharge` to `interp`	Maxime Dénès	2017-10-10
\|\ \
* \ \	Merge PR #1114: Generic handling of nameable objects for plugins	Maxime Dénès	2017-10-09
\|\ \ \
\| \| * \|	[deps] Move `Discharge` to `interp`	Emilio Jesus Gallego Arias	2017-10-09