coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	[warnings] Remove `set_current_loc` hack.	Emilio Jesus Gallego Arias	2018-04-11
\| \| \| \| \| \| \| \| \| \|	Instead of the current hack that won't work as soon as we check some part of the document asynchronously, we make the warning processor recover a proper location if the warning doesn't have one attached. This is what CoqIDE does [but it queries it's own document model]. Fixes: #6172
*	Merge PR #6955: Fixed many typos and grammar errors in chapter 11 of the manual.	Maxime Dénès	2018-04-11
\|\
* \	Merge PR #7020: Sphinx doc chapter 6	Théo Zimmermann	2018-04-10
\|\ \
\| * \|	[Sphinx] Add chapter 6	Maxime Dénès	2018-04-10
\| \| \| \| \| \| \| \| \| \| \| \|	Thanks to Yves Bertot for porting this chapter.
\| * \|	[Sphinx] Move chapter 6 to new infrastructure	Maxime Dénès	2018-04-10
\|/ /
* \|	Merge PR #7168: Sphinx doc chapter 15	Théo Zimmermann	2018-04-10
\|\ \
\| * \|	[Sphinx] Add chapter 15	Laurent Théry	2018-04-10
\| \| \| \| \| \| \| \| \| \| \| \|	Thanks to Laurent Théry for porting this chapter.
\| * \|	[Sphinx] Move chapter 15 to new infrastructure	Maxime Dénès	2018-04-10
\|/ /
* \|	Merge PR #7116: Fixes #7110: missing test on the absence of a "as" while ↵	Emilio Jesus Gallego Arias	2018-04-09
\|\ \ \| \| \| \| \| \| \| \| \|	looking for a notation for a nested pattern
* \ \	Merge PR #7103: Fix #7101: STM delegation policy broken	Enrico Tassi	2018-04-09
\|\ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	# Conflicts: # CHANGES
* \ \ \	Merge PR #7207: [ci] Tentative fix for #7206: MacOS test-suite job failing.	Gaëtan Gilbert	2018-04-09
\|\ \ \ \
\| * \| \| \|	[ci] Tentative fix for #7206: MacOS test-suite job failing.	Théo Zimmermann	2018-04-09
\|/ / / /
* \| \| \|	Merge PR #7162: Sphinx doc chapter 7	Théo Zimmermann	2018-04-09
\|\ \ \ \
* \ \ \ \	Merge PR #7176: Fix #6956: Uncaught exception in bytecode compilation	Pierre-Marie Pédrot	2018-04-09
\|\ \ \ \ \
* \ \ \ \ \	Merge PR #7070: Clarify wording in tactics documentation.	Maxime Dénès	2018-04-09
\|\ \ \ \ \ \
* \ \ \ \ \ \	Merge PR #7082: Expliciting and taking advantage of a representation ↵	Maxime Dénès	2018-04-09
\|\ \ \ \ \ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	invariant in Esubst
* \ \ \ \ \ \ \	Merge PR #7165: [ssr] check cleared hyps do exist (fix #7050)	Maxime Dénès	2018-04-09
\|\ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \	Merge PR #7184: [toplevel] Fix path initialization before vio processing ↵	Maxime Dénès	2018-04-09
\|\ \ \ \ \ \ \ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	(closes #7044)
\| \| \| \| \| \| * \| \| \|	[Sphinx] Add chapter 7	Maxime Dénès	2018-04-09
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Thanks to Laurent Théry for porting this chapter.
\| \| \| \| \| \| * \| \| \|	[Sphinx] Make it possible to espace { by %{ in custom grammars	Maxime Dénès	2018-04-09
\| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| * \| \| \|	[Sphinx] Move chapter 7 to new infrastructure	Maxime Dénès	2018-04-09
\| \|_\|_\|_\|_\|/ / / / \|/\| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \|	Merge PR #6809: Improve shell scripts	Michael Soegtrop	2018-04-08
\|\ \ \ \ \ \ \ \ \
\| \| * \| \| \| \| \| \| \|	[toplevel] Fix path initialization before vio processing (closes #7044)	Emilio Jesus Gallego Arias	2018-04-07
\| \|/ / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	The toplevel refactoring made path initialization per document, however vio-checking and vio-tasks are not documents, so loadpath must be initialized individually. Patch by @gares, refactoring to avoid double-initialization by me. Co-authored-by: <Enrico.Tassi@inria.fr>
\| \| \| \| \| \| \| \| *	Fixed many typos and grammar errors in chapter 11 of the manual.	Zeimer	2018-04-06
\| \| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \|	Merge PR #7129: Fix #7124: Warning "Ignoring implicit status" does not ↵	Hugo Herbelin	2018-04-06
\|\ \ \ \ \ \ \ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	provide line number
* \ \ \ \ \ \ \ \ \	Merge PR #6960: [api] Move some types to their proper module.	Pierre-Marie Pédrot	2018-04-06
\|\ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \	Merge PR #7180: Remove unused script.	Pierre-Marie Pédrot	2018-04-06
\|\ \ \ \ \ \ \ \ \ \ \ \| \|_\|_\|_\|_\|_\|_\|_\|_\|_\|/ \|/\| \| \| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \| \| \|	Merge PR #7178: Fixes issue #7172 (don't include MinGW make in install)	Enrico Tassi	2018-04-06
\|\ \ \ \ \ \ \ \ \ \ \
\| \| \| \| \| \| \| \| \| * \| \|	Fix #6956: Uncaught exception in bytecode compilation	Maxime Dénès	2018-04-06
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	We also make the code of [compact] in kernel/univ.ml a bit clearer.
* \| \| \| \| \| \| \| \| \| \| \|	Merge PR #7131: Sphinx doc chapter 30	Théo Zimmermann	2018-04-06
\|\ \ \ \ \ \ \ \ \ \ \ \
\| \| \| \| \| \| * \| \| \| \| \| \|	Improve shell scripts	zapashcanon	2018-04-05
\| \|_\|_\|_\|_\|/ / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \| \| \| \|	Merge PR #6838: Light refactoring of implicit arguments	Hugo Herbelin	2018-04-05
\|\ \ \ \ \ \ \ \ \ \ \ \
* \| \| \| \| \| \| \| \| \| \| \| \|	Refactor impargs code.	Jasper Hugunin	2018-04-05
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	This should preserve semantics exactly. In the compute_implicits family of functions, I changed the name of the pushed rel to not be fresh, but the env isn't passed to find_displayed_name_in, and shouldn't affect whd_all.
\| \| \| \| * \| \| \| \| \| \| \| \|	Remove unused script.	Théo Zimmermann	2018-04-05
\| \|_\|_\|/ / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	This is dead code since fd44a40f9d426a7b65f167bc30d320a0f7dd2bbd. This script was initially introduced in a088d03434417e935df3c75f81a954eadbdfc2b8 and left untouched since then.
\| \| \| \| \| * \| \| \| \| \| \|	Fix #7124: Warning "Ignoring implicit status" does not provide line number	Maxime Dénès	2018-04-05
\| \|_\|_\|_\|/ / / / / / / \|/\| \| \| \| \| \| \| \| \| \|
\| \| \| * \| \| \| \| \| \| \|	Fixes issue #7172 (don't include MinGW make in install)	Michael Soegtrop	2018-04-05
\| \| \| \| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \| \| \|	Merge PR #7169: Sphinx docs: fix typo in Chrząszcz (non-ASCII character ↵	Maxime Dénès	2018-04-05
\|\ \ \ \ \ \ \ \ \ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	lost in sphinx migration)
* \ \ \ \ \ \ \ \ \ \ \	Merge PR #7074: Update merging doc	Maxime Dénès	2018-04-05
\|\ \ \ \ \ \ \ \ \ \ \ \ \| \|_\|_\|_\|/ / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \|
\| * \| \| \| \| \| \| \| \| \| \|	Add note for homebrew users.	Théo Zimmermann	2018-04-05
\| \| \| \| \| \| \| \| \| \| \| \|
\| * \| \| \| \| \| \| \| \| \| \|	Some advice about merge script dependencies.	Théo Zimmermann	2018-04-05
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Including: how to create a GPG key.
\| * \| \| \| \| \| \| \| \| \| \|	Improve the MERGING doc.	Théo Zimmermann	2018-04-05
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	In particular, describes what to do with overlays.
\| * \| \| \| \| \| \| \| \| \| \|	Adapt CONTRIBUTING to recent changes in Coq.	Théo Zimmermann	2018-04-05
\|/ / / / / / / / / / / \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	- The testing and benchmarking labels are now distinct. - The release manager does not take care of merging anymore. - The reference manual is not written in LaTeX anymore.
* \| \| \| \| \| \| \| \| \| \|	Merge PR #7115: Sphinx doc chapter 28	Théo Zimmermann	2018-04-05
\|\ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \	Merge PR #7016: Make parsing independent of the cumulativity flag.	Enrico Tassi	2018-04-05
\|\ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #7139: [stm] More cleanup of "classification is not an interpreter"	Enrico Tassi	2018-04-05
\|\ \ \ \ \ \ \ \ \ \ \ \ \
\| \| \| \| \| \| * \| \| \| \| \| \| \|	[Sphinx] Add chapter 30	Maxime Dénès	2018-04-05
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Thanks to Paul Steckler for porting this chapter.
\| \| \| \| \| \| * \| \| \| \| \| \| \|	[Sphinx] Move chapter 30 to new infrastructure	Maxime Dénès	2018-04-05
\| \| \| \| \|_\|/ / / / / / / / \| \| \| \|/\| \| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \| \| \| \| \|	Merge PR #7127: Fix #6257: anomaly with Printing Projections and Context.	Hugo Herbelin	2018-04-04
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \| \|_\|_\|_\|_\|_\|_\|_\|_\|_\|/ / / \|/\| \| \| \| \| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \| \| \| \| \|	Merge PR #7163: merge-pr.sh: cache github API calls	Maxime Dénès	2018-04-04
\|\ \ \ \ \ \ \ \ \ \ \ \ \
\| \| \| \| \| \| * \| \| \| \| \| \| \|	Sphinx docs: fix typo (non-ASCII character lost in sphinx migration)	Peter LeFanu Lumsdaine	2018-04-04
\| \|_\|_\|_\|_\|/ / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \|