coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Separate vernac controls and regular commands.	Maxime Dénès	2017-12-20
*	Merge PR #6419: [vernac] Split `command.ml` into separate files.	Maxime Dénès	2017-12-18
\|\
* \	Merge PR #6413: [econstr] Switch constrintern API to non-imperative style.	Maxime Dénès	2017-12-18
\|\ \
\| \| *	[flags] Make program_mode a parameter for commands in vernac.	Emilio Jesus Gallego Arias	2017-12-17
\| \| *	[vernac] Split `command.ml` into separate files.	Emilio Jesus Gallego Arias	2017-12-17
\| \|/
* \|	Merge PR #6392: [econstr] Cleanup in `vernac/classes.ml`	Maxime Dénès	2017-12-15
\|\ \
\| \| *	[econstr] Switch constrintern API to non-imperative style.	Emilio Jesus Gallego Arias	2017-12-15
* \| \|	Merge PR #6341: Fix anomaly in [Type foo] command, + print uctx like Check.	Maxime Dénès	2017-12-13
\|\ \ \
* \ \ \	Merge PR #6251: [proof] Embed evar_map in RefinerError exception.	Maxime Dénès	2017-12-13
\|\ \ \ \
\| \| \| \| *	[econstr] Small cleanup in `vernac/lemmas`	Emilio Jesus Gallego Arias	2017-12-13
\| \| \| \|/
\| \| \| *	[econstr] Cleanup in `vernac/classes.ml`.	Emilio Jesus Gallego Arias	2017-12-13
\| \|_\|/ \|/\| \|
* \| \|	Merge PR #6275: [summary] Allow typed projections from global state.	Maxime Dénès	2017-12-12
\|\ \ \
* \ \ \	Merge PR #6270: [toplevel] Properly redirect stdout on `Redirect` vernac.	Maxime Dénès	2017-12-11
\|\ \ \ \
\| \| \| \| *	Fix anomaly in [Type foo] command, + print uctx like Check.	Gaëtan Gilbert	2017-12-11
\| \| \| * \|	[proof] Embed evar_map in RefinerError exception.	Emilio Jesus Gallego Arias	2017-12-11
\| \|_\|/ / \|/\| \| \|
* \| \| \|	Merge PR #6324: Fix #6323: stronger restrict universe context vs abstract.	Maxime Dénès	2017-12-11
\|\ \ \ \
* \| \| \| \|	[api] Remove kernel dependency on intf (Decl_kind)	Emilio Jesus Gallego Arias	2017-12-10
\| \|_\|_\|/ \|/\| \| \|
\| \| \| *	[summary] Adapt STM to the new Summary API.	Emilio Jesus Gallego Arias	2017-12-09
\| \| \| *	[summary] Allow typed projections from global state + rework of internals.	Emilio Jesus Gallego Arias	2017-12-09
\| \|_\|/ \|/\| \|
\| * \|	Fix #6323: stronger restrict universe context vs abstract.	Gaëtan Gilbert	2017-12-06
\|/ /
* \|	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
\|\ \ \ \
\| \| \| \| *	[toplevel] Properly redirect stdout on `Redirect` vernac.	Emilio Jesus Gallego Arias	2017-11-28
\| \|_\|_\|/ \|/\| \| \|
\| \| * \|	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