coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Adding a custom Travis overlay for HoTT.	Pierre-Marie Pédrot	2018-01-11
\|
*	Merge PR #6493: [API] remove large file containing duplicate interfaces	Maxime Dénès	2017-12-29
\|\
\| *	overlay for #6493	Enrico Tassi	2017-12-27
\| \|
* \|	Add equations overlay.	Maxime Dénès	2017-12-27
\|/
*	Fix overlay selection for Circle CI.	Gaëtan Gilbert	2017-12-26
\|
*	Delete old overlays (leaving example)	Gaëtan Gilbert	2017-12-26
\|
*	Merge PR #6217: Do dependencies in 1 command per file class.	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
\|\ \
\| \| *	Overlay for unimath.	Gaëtan Gilbert	2017-12-15
\| \| \|
* \| \|	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
\| \|/ / \| \| \| \| \| \| \| \| \| \| \| \|	We remove a lot of uses of `evar_map` ref in `vernac`, cleanup step desirable to progress with EConstr there.
\| * \|	[econstr] Cleanup in `vernac/classes.ml`.	Emilio Jesus Gallego Arias	2017-12-13
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	We fix quite a few types, and perform some cleanup wrt to the evar_map, in particular we prefer to thread it now as otherwise it may become trickier to check when we are using the correct one. Thanks to @SkySkimmer for lots of comments and bug-finding.
* \| \|	Add overlay.	Théo Zimmermann	2017-12-11
\|/ /
* \|	Merge PR #6324: Fix #6323: stronger restrict universe context vs abstract.	Maxime Dénès	2017-12-11
\|\ \
* \ \	Merge PR #6158: Allows a level in the raw and glob printers	Maxime Dénès	2017-12-08
\|\ \ \ \| \|_\|/ \|/\| \|
\| \| *	Overlay for Equations.	Gaëtan Gilbert	2017-12-06
\| \|/ \|/\|
\| *	Adding overlay for ltac2.	Hugo Herbelin	2017-11-27
\| \|
* \|	Overlay for stronger restrict_universe_context.	Gaëtan Gilbert	2017-11-25
\|/
*	[plugin] Remove LocalityFixme über hack.	Emilio Jesus Gallego Arias	2017-11-22
\| \| \| \| \| \| \| \| \| \|	To that extent we introduce a new prototype vernacular extension macro `VERNAC COMMAND FUNCTIONAL EXTEND` that will take a function with the proper parameters and attributes. This of course needs more refinement, in particular we should move `vernac_command` to its own file and make `Vernacentries` consistent wrt it.
*	Each user overlay goes into its own file.	Théo Zimmermann	2017-06-16
	This will avoid stupid merge conflicts in the future.