coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Merge PR #6331: Linter: skip PRs older than the linter.	Maxime Dénès	2017-12-11
\|\
* \	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
\|\ \ \
* \ \ \	Merge PR #6358: [ci] Download ci-sf archives into the proper CI build dir.	Maxime Dénès	2017-12-11
\|\ \ \ \
* \ \ \ \	Merge PR #6351: Fix a copy-paste error in ci-ltac2.	Maxime Dénès	2017-12-11
\|\ \ \ \ \
* \ \ \ \ \	Merge PR #6346: [ci] CoLoR has moved to github	Maxime Dénès	2017-12-11
\|\ \ \ \ \ \
* \| \| \| \| \| \|	[ci] Temporal workaround for checker non-backwards compatible change.	Emilio Jesus Gallego Arias	2017-12-10
\| \| \| \| \| \| \|
\| \| \| \| \| * \|	[api] Remove yet another type alias.	Emilio Jesus Gallego Arias	2017-12-09
\| \|_\|_\|_\|/ / \|/\| \| \| \| \|
\| \| \| * \| \|	[ci] Download ci-sf archives into the proper CI build dir.	Emilio Jesus Gallego Arias	2017-12-09
\| \|_\|/ / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Currently, `make ci-sf` downloads and builds the files in the main root directory. we fix that.
\| \| * \| \|	Fix a copy-paste error in ci-ltac2.	Théo Zimmermann	2017-12-08
\| \| \| \| \|
* \| \| \| \|	Merge PR #6158: Allows a level in the raw and glob printers	Maxime Dénès	2017-12-08
\|\ \ \ \ \
\| \| * \| \| \|	[ci] CoLoR has moved to github	Emilio Jesus Gallego Arias	2017-12-07
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Closes #6194 .
* \| \| \| \| \|	Merge PR #6267: Fix PR merge script.	Maxime Dénès	2017-12-07
\|\ \ \ \ \ \ \| \|_\|/ / / / \|/\| \| \| \| \|
\| \| \| \| * \|	Overlay for Equations.	Gaëtan Gilbert	2017-12-06
\| \|_\|_\|/ / \|/\| \| \| \|
\| \| \| \| *	Linter: skip PRs older than the linter.	Gaëtan Gilbert	2017-12-06
\| \|_\|_\|/ \|/\| \| \|
* \| \| \|	uninstall doc dir, not dev (which is not installed), #6007	Paul Steckler	2017-12-01
\| \| \| \|
* \| \| \|	Merge PR #736: [ci] Test coqchk on the CompCert target.	Maxime Dénès	2017-12-01
\|\ \ \ \
* \ \ \ \	Merge PR #6244: [lib] [api] Introduce record for `object_prefix`	Maxime Dénès	2017-11-30
\|\ \ \ \ \
\| \| * \| \| \|	[ci] Test coqchk on the CompCert target.	Théo Zimmermann	2017-11-30
\| \|/ / / / \|/\| \| \| \|
* \| \| \| \|	Merge PR #6269: [ci] [vst] Shorten compilation time to avoid Travis timeouts.	Maxime Dénès	2017-11-30
\|\ \ \ \ \
\| \| \| * \| \|	Fix usage comment.	Théo Zimmermann	2017-11-29
\| \| \| \| \| \|
\| \| \| * \| \|	This script apparently uses bash-specific features.	Théo Zimmermann	2017-11-29
\| \| \| \| \| \|
\| \| \| * \| \|	Fix PR merge script.	Théo Zimmermann	2017-11-29
\| \|_\|/ / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \|	Was still relying on the existence of user-configured /pr/.
\| \| * \| \|	[lib] [api] Introduce record for `object_prefix`	Emilio Jesus Gallego Arias	2017-11-29
\| \| \| \|/ \| \| \|/\| \| \| \| \| \| \| \| \| \| \| \| \|	This is a minor cleanup adding a record in a try to structure the state living in `Lib`.
* \| \| \|	Add PR backport script.	Théo Zimmermann	2017-11-28
\| \| \| \|
\| * \| \|	[ci] [vst] Shorten compilation time to avoid Travis timeouts.	Emilio Jesus Gallego Arias	2017-11-28
\|/ / / \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	We remove the progs target [examples] to save time, we still build the full library thou. I guess we can't do better for now unless we get some Travis subscription.
* \| \|	Merge PR #6259: Add PR merge script.	Maxime Dénès	2017-11-28
\|\ \ \
\| * \| \|	Add PR merge script.	Maxime Dénès	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
\|\ \ \ \ \| \|_\|/ / \|/\| \| \|
\| \| \| *	Adding overlay for ltac2.	Hugo Herbelin	2017-11-27
\| \| \| \|
* \| \| \|	Merge PR #6227: Linter: do not lint untracked files.	Maxime Dénès	2017-11-27
\|\ \ \ \ \| \|_\|_\|/ \|/\| \| \|
\| \| * \|	[api] Remove aliases of `Evar.t`	Emilio Jesus Gallego Arias	2017-11-26
\| \|/ / \|/\| \| \| \| \| \| \| \| \| \| \|	There don't really bring anything, we also correct some minor nits with the printing function.
\| \| *	Overlay for stronger restrict_universe_context.	Gaëtan Gilbert	2017-11-25
\| \|/ \|/\|
* \|	Merge PR #876: In omega or romega, recognizing Z and nat modulo conversion	Maxime Dénès	2017-11-24
\|\ \
* \ \	Merge PR #6197: [plugin] Remove LocalityFixme über hack.	Maxime Dénès	2017-11-24
\|\ \ \
* \ \ \	Merge PR #6186: [api] Miscellaneous consolidation.	Maxime Dénès	2017-11-23
\|\ \ \ \
\| \| \| \| *	Linter: do not lint untracked files.	Gaëtan Gilbert	2017-11-23
\| \|_\|_\|/ \|/\| \| \|
\| \| \| *	Adding ad hoc overlay for sf/vfa.	Hugo Herbelin	2017-11-23
\| \|_\|/ \|/\| \|
* \| \|	Merge PR #6189: Disable whitespace linter for .out files.	Maxime Dénès	2017-11-23
\|\ \ \
\| \| \| *	[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.
\| \| *	[api] Miscellaneous consolidation + moves to engine.	Emilio Jesus Gallego Arias	2017-11-21
\| \|/ \|/\| \| \| \| \| \| \| \| \|	We deprecate a few functions that were deprecated in the comments plus we place `Nameops` and `Univops` in engine where they do seem to belong in the large picture of code organization.
* \|	[printing] Deprecate all printing functions accessing the global proof.	Emilio Jesus Gallego Arias	2017-11-21
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	We'd like to handle proofs functionally we thus recommend not to use printing functions without an explicit context. We also adapt most of the code, making more explicit where the printing environment is coming from. An open task is to refactor some code so we gradually make the `Pfedit.get_current_context ()` disappear.
* \|	Merge PR #6185: [parser] Remove unnecessary statically initialized hook.	Maxime Dénès	2017-11-21
\|\ \
* \ \	Merge PR #6168: Add Equations to CI	Maxime Dénès	2017-11-21
\|\ \ \
\| \| \| *	Disable whitespace linter for .out files.	Gaëtan Gilbert	2017-11-20
\| \| \| \|
* \| \| \|	Merge PR #6183: [plugins] Prepare plugin API for functional handling of state.	Maxime Dénès	2017-11-20
\|\ \ \ \
* \ \ \ \	Merge PR #6163: [dev] Remove deprecation warning from `base_include`	Maxime Dénès	2017-11-20
\|\ \ \ \ \ \| \|_\|_\|_\|/ \|/\| \| \| \|
\| \| \| * \|	Add Equations to CI	Matthieu Sozeau	2017-11-20
\| \|_\|/ / \|/\| \| \|
\| \| \| *	[parser] Remove unnecessary statically initialized hook.	Emilio Jesus Gallego Arias	2017-11-19
\| \|_\|/ \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Addded by c6d9d4fb142ef42634be25b60c0995b541e86629 ["Adding ability to put any pattern in binders, prefixed by a quote."] its current placement as well as the hook don't make a lot of sense. In particular, they prevent parts of Coq working without linking the parser. To this purpose, we need to consolidate the `Constrexpr` utilities. While we are at it we do so and remove the `Topconstr` module which is fully redundant with `Constrexpr_ops`.