coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Add a comment on EConstr.to_constr regarding evar-freeness.	Pierre-Marie Pédrot	2018-02-27
*	[ast] Improve precision of Ast location recognition in serialization.	Emilio Jesus Gallego Arias	2018-02-22
*	[engine] Remove ghost parameter from `Proofview.Goal.t`	Emilio Jesus Gallego Arias	2018-02-12
*	Merge PR #6262: [error] Replace msg_error by a proper exception.	Maxime Dénès	2018-02-12
\|\
* \|	Simplification: cumulativity information is variance information.	Gaëtan Gilbert	2018-02-10
\| *	[error] Replace msg_error by a proper exception.	Emilio Jesus Gallego Arias	2018-02-09
\|/
*	Merge PR #6675: [proofview] enter_one: add __LOC__ argument to get relevant e...	Maxime Dénès	2018-02-01
\|\
\| *	Proofview: enter_one: add __LOC__ argument to get relevant error msg	Enrico Tassi	2018-01-31
* \|	Merge PR #6535: Cleanup name-binding structure for fresh evar name generation.	Maxime Dénès	2018-01-31
\|\ \
* \ \	Merge PR #6618: Fix Ltac subterm matching in (co-)fixpoints.	Maxime Dénès	2018-01-22
\|\ \ \ \| \|_\|/ \|/\| \|
\| * \|	Define EConstr version of [push_rec_types].	Cyprien Mangin	2018-01-19
* \| \|	Merge PR #6555: Use let-in aware prod_applist_assum in dtauto and firstorder.	Maxime Dénès	2018-01-18
\|\ \ \ \| \|/ / \|/\| \|
* \| \|	Merge PR #6298: Fix #6297: handle constraints like (u+1 <= Set/Prop)	Maxime Dénès	2018-01-17
\|\ \ \
\| \| * \|	Add a test that `prod_applist_assum` reduces the right number of let-ins	Jasper Hugunin	2018-01-17
\| \| * \|	Use let-in aware prod_applist_assum in dtauto and firstorder.	Jasper Hugunin	2018-01-17
\| \|/ / \|/\| \|
\| \| *	Use a more efficient substitution composition in evar hypothesis naming.	Pierre-Marie Pédrot	2018-01-04
\| \| *	Cleanup name-binding structure for fresh evar name generation.	Pierre-Marie Pédrot	2018-01-02
* \| \|	Moving some universe substitution code out of the kernel.	Pierre-Marie Pédrot	2017-12-30
\| \|/ \|/\|
* \|	Merge PR #6222: Share computation of unifiable evars	Maxime Dénès	2017-12-22
\|\ \
* \ \	Merge PR #6413: [econstr] Switch constrintern API to non-imperative style.	Maxime Dénès	2017-12-18
\|\ \ \
* \ \ \	Merge PR #6392: [econstr] Cleanup in `vernac/classes.ml`	Maxime Dénès	2017-12-15
\|\ \ \ \
* \ \ \ \	Merge PR #6038: [build] Remove coqmktop in favor of ocamlfind.	Maxime Dénès	2017-12-14
\|\ \ \ \ \
\| \| \| * \| \|	[econstr] Add a couple of new API functions.	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 #6368: [api] Remove yet another type alias.	Maxime Dénès	2017-12-11
\|\ \ \ \ \
* \ \ \ \ \	Merge PR #6324: Fix #6323: stronger restrict universe context vs abstract.	Maxime Dénès	2017-12-11
\|\ \ \ \ \ \
\| \| * \| \| \| \|	[api] Remove yet another type alias.	Emilio Jesus Gallego Arias	2017-12-09
\| \|/ / / / / \|/\| \| \| \| \|
\| \| \| * \| \|	[lib] Rename Profile to CProfile	Emilio Jesus Gallego Arias	2017-12-09
\| \|_\|/ / / \|/\| \| \| \|
\| \| * \| \|	[summary] Adapt STM to the new Summary API.	Emilio Jesus Gallego Arias	2017-12-09
\| \|/ / / \|/\| \| \|
* \| \| \|	Merge PR #6290: Rename update to set, Fixes #6196	Maxime Dénès	2017-12-07
\|\ \ \ \
\| \| * \| \|	Fix #6323: stronger restrict universe context vs abstract.	Gaëtan Gilbert	2017-12-06
\| \|/ / / \|/\| \| \|
\| * \| \|	Rename update to set, fixes #6196	Paul Steckler	2017-12-05
\| \| \| *	Fix #6297: handle constraints like (u+1 <= Set/Prop)	Gaëtan Gilbert	2017-12-01
\| \| \|/ \| \|/\|
* \| \|	Cleanup API for registering universe binders.	Matthieu Sozeau	2017-12-01
* \| \|	Proper nametab handling of global universe names	Matthieu Sozeau	2017-12-01
\|/ /
* \|	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
\|\ \ \
\| * \| \|	[api] Remove aliases of `Evar.t`	Emilio Jesus Gallego Arias	2017-11-26
\| \| * \|	Forbid repeated names in universe binders.	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
\| \| * \|	Make restrict_universe_context stronger.	Gaëtan Gilbert	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
\| * \|	restrict_universe_context: do not prune named universes.	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
\| * \|	Use type Universes.universe_binders.	Gaëtan Gilbert	2017-11-24
\|/ /