coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	[vernac] vernac_expr no longer recursive	Vincent Laporte	2018-01-08
*	[vernac] adds the “program” flag to the “atts” record	Vincent Laporte	2017-12-29
*	Merge PR #6492: Remove query-in-IDE warning.	Maxime Dénès	2017-12-29
\|\
* \	Merge PR #6405: Remove the local polymorphic flag hack.	Maxime Dénès	2017-12-29
\|\ \
* \ \	Merge PR #6433: [flags] Move global time flag into an attribute.	Maxime Dénès	2017-12-29
\|\ \ \
\| \| \| *	Remove query-in-IDE warning.	Maxime Dénès	2017-12-27
\| \|_\|/ \|/\| \|
\| \| *	Remove the local polymorphic flag hack.	Maxime Dénès	2017-12-27
\| \|/ \|/\|
* \|	Merge PR #6439: [api] Also deprecate constructors of Decl_kinds.	Maxime Dénès	2017-12-27
\|\ \
* \ \	Merge PR #6443: [vernac] Cleanup of do_definition.	Maxime Dénès	2017-12-27
\|\ \ \
* \ \ \	Merge PR #6289: Remove unused boolean from cl_context field of Typeclasses.ty...	Maxime Dénès	2017-12-27
\|\ \ \ \
\| \| \| * \|	[api] Also deprecate constructors of Decl_kinds.	Emilio Jesus Gallego Arias	2017-12-23
\| \|_\|/ / \|/\| \| \|
\| \| \| *	[flags] Move global time flag into an attribute.	Emilio Jesus Gallego Arias	2017-12-23
\| \|_\|/ \|/\| \|
\| \| *	Merge code paths in interp_definition and cleanup a bit.	Gaëtan Gilbert	2017-12-21
* \| \|	Separate vernac controls and regular commands.	Maxime Dénès	2017-12-20
\| \| *	[vernac] Cleanup of do_definition.	Emilio Jesus Gallego Arias	2017-12-18
\| \|/ \|/\|
* \|	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
\|\ \ \ \ \
\| \| \| \| \| *	Remove unused boolean from cl_context field of Typeclasses.typeclass	Gaëtan Gilbert	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
\|\ \ \ \ \| \|_\|_\|/ \|/\| \| \|