coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Merge PR #942: solving b1859	Maxime Dénès	2017-08-16
\|\
* \	Merge PR #954: Print names of all open blocks	Maxime Dénès	2017-08-16
\|\ \
* \ \	Merge PR #964: More portable location for the time command.	Maxime Dénès	2017-08-16
\|\ \ \
* \ \ \	Merge PR #951: Makefile: install-byte works even if -coqide no	Maxime Dénès	2017-08-16
\|\ \ \ \
* \ \ \ \	Merge PR #841: Timorous fix of bug #5598 on global existing class in sections	Maxime Dénès	2017-08-16
\|\ \ \ \ \
* \ \ \ \ \	Merge PR #948: [doc] Write (@nil nat) instead of (nil nat)	Maxime Dénès	2017-08-16
\|\ \ \ \ \ \
* \ \ \ \ \ \	Merge PR #944: Fix typos. Improve wording.	Maxime Dénès	2017-08-16
\|\ \ \ \ \ \ \
* \ \ \ \ \ \ \	Merge PR #943: Reference Manual: minor wording improvements	Maxime Dénès	2017-08-16
\|\ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \	Merge PR #940: Replace jarring use of "Remark" with "Note"	Maxime Dénès	2017-08-16
\|\ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \	Merge PR #934: Fix some coq-tex errors in the reference manual.	Maxime Dénès	2017-08-16
\|\ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \	Merge PR #880: Fix coqdoc bug #5648 on user idents colliding with keywords ↵	Maxime Dénès	2017-08-16
\|\ \ \ \ \ \ \ \ \ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	wrongly tagged as keywords
* \ \ \ \ \ \ \ \ \ \ \	Merge PR #864: Some cleanups after cumulativity for inductive types	Maxime Dénès	2017-08-16
\|\ \ \ \ \ \ \ \ \ \ \ \
\| \| \| \| \| \| \| \| \| \| \| \| *	Adding a test for BZ#1859 as suggested by @tchajed.	Théo Zimmermann	2017-08-15
\| \| \| \| \| \| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \| \| \| \| \|	Merge PR #963: fix coq_makefile	Maxime Dénès	2017-08-12
\|\ \ \ \ \ \ \ \ \ \ \ \ \
\| * \| \| \| \| \| \| \| \| \| \| \| \|	fix coq_makefile	Matej Košík	2017-08-12
\|/ / / / / / / / / / / / / \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Make sure that when plugin writer does not use -bypass-API, API is opened by default.
\| \| \| \| \| \| \| \| \| \| * / /	More portable location for the time command.	Théo Zimmermann	2017-08-12
\| \|_\|_\|_\|_\|_\|_\|_\|_\|/ / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	On NixOS in particular, /usr/bin/time doesn't exist.
\| \| \| \| \| \| \| \| \| \| * \|	Print names of all open blocks	Tej Chajed	2017-08-06
\| \|_\|_\|_\|_\|_\|_\|_\|_\|/ / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Fixes bug 5597.
\| \| \| \| \| \| \| \| \| * \|	Makefile: install-byte works even if -coqide no	Enrico Tassi	2017-08-04
\| \|_\|_\|_\|_\|_\|_\|_\|/ / \|/\| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| * \| \| \|	Amend wording to capture intended meaning	Sam Pablo Kuper	2017-08-03
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	per @Zimmi48's comments [here](https://github.com/coq/coq/pull/944#discussion_r131072333) and [here](https://github.com/coq/coq/pull/944#discussion_r131072790).
\| \| \| \| \| \| \| * \| \|	Update Setoid.tex	larsr	2017-08-02
\| \|_\|_\|_\|_\|_\|/ / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	The term of type `list nat` should be `(@nil nat)` instead of `(nil nat)`.
* \| \| \| \| \| \| \| \|	Makefile: 'make clean' now immune to the check for binary files without sources	Pierre Letouzey	2017-08-02
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	This is a followup of 7d1fc15. Without this fix, you're warned of leftover files, but even a 'make clean' is then refused, so you cannot get rid of them easily (apart via a git clean -xfd).
\| * \| \| \| \| \| \| \|	Typo in the documentation of cumulativity	Amin Timany	2017-08-02
\| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| * \| \|	Fix typos. Improve wording.	Sam Pablo Kuper	2017-08-01
\| \| \| \| \| \| \| \| \|
\| \| \| \| * \| \| \| \|	Improve style slightly	Sam Pablo Kuper	2017-08-01
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	per @aspiwack's comments in [this pull request review](https://github.com/coq/coq/pull/940).
* \| \| \| \| \| \| \| \|	Merge PR #933: Fix documentation of Hint Mode (bug #4911).	Maxime Dénès	2017-08-01
\|\ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \	Merge PR #932: Fix shuffled documentation.	Maxime Dénès	2017-08-01
\|\ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \	Merge PR #929: Add missing paragraph to introduction	Maxime Dénès	2017-08-01
\|\ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \	Merge PR #928: Fixing bug #5671 (tactic specialize unclean wrt Metas).	Maxime Dénès	2017-08-01
\|\ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #926: test-suite uses Extraction TestCompile	Maxime Dénès	2017-08-01
\|\ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #925: Document Extraction TestCompile	Maxime Dénès	2017-08-01
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #921: [make] remove compat5 file.	Maxime Dénès	2017-08-01
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #919: Remove a few useless evar-normalizations in printing code.	Maxime Dénès	2017-08-01
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #917: Moving --print-version to -print-version for consistency.	Maxime Dénès	2017-08-01
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #913: Less allocations in Detyping	Maxime Dénès	2017-08-01
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #909: Extraction: reduce primitive projections in types (fix bug 4709)	Maxime Dénès	2017-08-01
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #893: Removing default evar-normalization for ARGUMENT EXTEND.	Maxime Dénès	2017-08-01
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #834: Adding support for recursive notations of the form "x , .. , ↵	Maxime Dénès	2017-08-01
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	y , z".
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #806: closing bug 5315	Maxime Dénès	2017-08-01
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #775: [toplevel] Remove long ago deprecated and NOOP options.	Maxime Dénès	2017-08-01
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| *	adding a comment to explain the change	Julien Forest	2017-08-01
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| *	solving b1859	Julien Forest	2017-08-01
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|/ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|/\|
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| * \| \|	Fix incorrect use of "At the end".	Sam Pablo Kuper	2017-07-31
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| * \| \|	Minor grammar fix: replace a "then" with a "so".	Sam Pablo Kuper	2017-07-31
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|/ /
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| * / /	Replace jarring use of "Remark" with "Note"	Sam Pablo Kuper	2017-07-31
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|/ / \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	or with nothing at all, to improve readability for native English speakers. Editors may wish to remove such constructions altogether in future revisions, per general style guidance such as: - https://en.wikipedia.org/wiki/Wikipedia:%22Note_that%22_is_unnecessary - https://english.stackexchange.com/a/238142/7318 - http://blog.apastyle.org/apastyle/2015/09/principles-of-writing-how-to-avoid-wordiness.html
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| * \| \| \| \|	Update documentation of cumulativity	Amin Timany	2017-07-31
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| * \| \| \| \|	Improve errors for cumulativity when monomorphic	Amin Timany	2017-07-31
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	We now only issue an error for locally specified (non)cumulativity whenever it is the context (set locally or globally) is monorphic.
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| * \| \| \| \|	Change the option for cumulativity	Amin Timany	2017-07-31
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| * \| \| \| \|	Fix typo and Add Jason's example to the doc	Amin Timany	2017-07-31
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| * \| \| \| \|	Improve documentation of cumulativity	Amin Timany	2017-07-31
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| * \| \| \| \|	Add Jason's example of fun-ext with cumulativity	Amin Timany	2017-07-31
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|