coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	[api] Move bullets and goals selectors to `proofs/`	Emilio Jesus Gallego Arias	2018-05-01
*	Evar maps contain econstrs.	Gaëtan Gilbert	2018-04-13
*	[located] More work towards using CAst.t	Emilio Jesus Gallego Arias	2018-03-09
*	Cosmetic: add an expected newline in proof_global.	Hugo Herbelin	2018-03-08
*	Rename some universe minimizing "normalize" functions to "minimize"	Gaëtan Gilbert	2018-03-06
*	Deprecate UState aliases in Evd.	Gaëtan Gilbert	2018-03-06
*	Update headers following #6543.	Théo Zimmermann	2018-02-27
*	[ast] Improve precision of Ast location recognition in serialization.	Emilio Jesus Gallego Arias	2018-02-22
*	[toplevel] Make toplevel state into a record.	Emilio Jesus Gallego Arias	2018-02-15
*	Fix #6591: anomaly when using selectors outside of a proof.	Cyprien Mangin	2018-01-22
*	Force polymorphic definitions to have no internal constraints.	Pierre-Marie Pédrot	2018-01-11
*	Fix #6323: stronger restrict universe context vs abstract.	Gaëtan Gilbert	2017-12-06
*	Cleanup API for registering universe binders.	Matthieu Sozeau	2017-12-01
*	[proof] [api] Rename proof types in preparation for functionalization.	Emilio Jesus Gallego Arias	2017-11-29
*	Make restrict_universe_context stronger.	Gaëtan Gilbert	2017-11-25
*	In close_proof only check univ decls with the restricted context.	Gaëtan Gilbert	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
*	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
*	[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
*	[api] Move structures deprecated in the API to the core.	Emilio Jesus Gallego Arias	2017-11-06
*	[stm] Remove state-handling from Futures.	Emilio Jesus Gallego Arias	2017-10-17
*	proof_global: cleanup and comment close_proof	Matthieu Sozeau	2017-09-19
*	Allow declaring universe constraints at definition level.	Matthieu Sozeau	2017-09-19
*	More precise type for universe entries.	Pierre-Marie Pédrot	2017-07-26
*	Merge PR #770: [proof] Move bullets to their own module.	Maxime Dénès	2017-07-19
\|\
* \|	Bump year in headers.	Pierre-Marie Pédrot	2017-07-04
* \|	Remove Warnings: unused value ...	Amin Timany	2017-06-16
* \|	Squashed commit of the following:	Amin Timany	2017-06-16
\| *	[proof] Move bullets to their own module.	Emilio Jesus Gallego Arias	2017-06-12
\|/
*	Drop '.' from CErrors.anomaly, insert it in args	Jason Gross	2017-06-02
*	[cleanup] Unify all calls to the error function.	Emilio Jesus Gallego Arias	2017-05-27
*	Merge PR#481: [option] Remove support for non-synchronous options.	Maxime Dénès	2017-05-25
\|\
* \	Merge branch 'trunk' into located_switch	Emilio Jesus Gallego Arias	2017-05-24
\|\ \
\| \| *	[option] Remove support for non-synchronous options.	Emilio Jesus Gallego Arias	2017-05-24
\| * \|	Merge PR#642: Small cleanup on `close_proof` type.	Maxime Dénès	2017-05-24
\| \|\ \ \| \| \|/ \| \|/\|
\| \| *	[vernac] Remove `Save thm id.` command.	Emilio Jesus Gallego Arias	2017-05-23
\| * \|	Change wrong bullet message.	Théo Zimmermann	2017-05-20
\| \|/
* \|	[location] Make location optional in Loc.located	Emilio Jesus Gallego Arias	2017-04-25
* \|	[location] Remove Loc.ghost.	Emilio Jesus Gallego Arias	2017-04-25
\|/
*	Merge PR#552: Miscelaneous commits	Maxime Dénès	2017-04-24
\|\
* \|	Remove VernacError	Gaetan Gilbert	2017-04-21
\| *	COMMENT: Proof_global.pstate.pid	Matej Kosik	2017-04-20
\|/
*	Merge branch 'trunk' into pr379	Maxime Dénès	2017-03-24
\|\
\| *	[pp] [ide] Minor cleanups in pp code.	Emilio Jesus Gallego Arias	2017-03-21
\| *	[stm] Break stm/toplevel dependency loop.	Emilio Jesus Gallego Arias	2017-02-15
* \|	Merge branch 'master'.	Pierre-Marie Pédrot	2017-02-14
\|\\|
* \|	Evar-normalizing functions now act on EConstrs.	Pierre-Marie Pédrot	2017-02-14