coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Fix anomaly in [Type foo] command, + print uctx like Check.	Gaëtan Gilbert	2017-12-11
*	Merge PR #890: Global universe declarations	Maxime Dénès	2017-12-05
\|\
* \|	[vernac] Couple of tweaks missing from previous PRs.	Emilio Jesus Gallego Arias	2017-12-04
\| *	Cleanup API for registering universe binders.	Matthieu Sozeau	2017-12-01
\|/
*	Merge PR #6233: [proof] [api] Rename proof types in preparation for functiona...	Maxime Dénès	2017-12-01
\|\
* \	Merge PR #1049: Remove obsolete locality	Maxime Dénès	2017-11-30
\|\ \
* \ \	Merge PR #6244: [lib] [api] Introduce record for `object_prefix`	Maxime Dénès	2017-11-30
\|\ \ \
* \ \ \	Merge PR #6193: Fix (partial) #4878: option to stop autodeclaring axiom as in...	Maxime Dénès	2017-11-30
\|\ \ \ \
\| \| \| * \|	Remove "obsolete_locality" and fix STM vernac classification.	Maxime Dénès	2017-11-29
\| \|_\|/ / \|/\| \| \|
\| \| * \|	[lib] [api] Introduce record for `object_prefix`	Emilio Jesus Gallego Arias	2017-11-29
\| \| \| *	[proof] [api] Rename proof types in preparation for functionalization.	Emilio Jesus Gallego Arias	2017-11-29
\| \|_\|/ \|/\| \|
* \| \|	Merge PR #6199: [vernac] Uniformize type of vernac interpretation.	Maxime Dénès	2017-11-29
\|\ \ \
\| \| * \|	Fix (partial) #4878: option to stop autodeclaring axiom as instance.	Gaëtan Gilbert	2017-11-28
\| \|/ / \|/\| \|
* \| \|	Merge PR #1033: Universe binder improvements	Maxime Dénès	2017-11-28
\|\ \ \
* \ \ \	Merge PR #6248: [api] Remove aliases of `Evar.t`	Maxime Dénès	2017-11-28
\|\ \ \ \ \| \|_\|_\|/ \|/\| \| \|
\| \| \| *	[vernac] Adjust `interp` to pass polymorphic in the attributes.	Emilio Jesus Gallego Arias	2017-11-27
\| \| \| *	[vernac] Add polymorphic to the type of vernac interpration options.	Emilio Jesus Gallego Arias	2017-11-27
\| \| \| *	[vernac] Start to uniformize type of vernac interpretation.	Emilio Jesus Gallego Arias	2017-11-27
\| \|_\|/ \|/\| \|
* \| \|	Merge PR #6241: [lib] Generalize Control.timeout type.	Maxime Dénès	2017-11-27
\|\ \ \
* \ \ \	Merge PR #6041: Protecting the printing of filenames with space	Maxime Dénès	2017-11-27
\|\ \ \ \
\| \| \| * \|	[api] Remove aliases of `Evar.t`	Emilio Jesus Gallego Arias	2017-11-26
\| \|_\|/ / \|/\| \| \|
\| \| \| *	Restrict universe context when declaring constants in obligations.	Gaëtan Gilbert	2017-11-25
\| \| \| *	Fix #5347: unify declaration of axioms with and without bound univs.	Gaëtan Gilbert	2017-11-25
\| \| \| *	Universe binders survive sections, modules and compilation.	Gaëtan Gilbert	2017-11-25
\| \| \| *	Allow local universe renaming in Print.	Gaëtan Gilbert	2017-11-25
\| \| \| *	Fix obligations handling of universes anticipating stronger restrict	Matthieu Sozeau	2017-11-25
\| \| * \|	[lib] Generalize Control.timeout type.	Emilio Jesus Gallego Arias	2017-11-24
\| \|/ / \|/\| \|
\| \| *	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
\|\ \
\| \| *	Quote file names which have spaces in "Print LoadPath".	Hugo Herbelin	2017-11-23
\| \|/ \|/\|
* \|	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
\| \|/ / \|/\| \|