coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
...
\| \| \| \| \| *	[flags] Remove XML output flag.	Emilio Jesus Gallego Arias	2017-08-01
\| \|_\|_\|_\|/ \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	This is a second try at removing the hooks for the legacy xml export system which can't currently be tested. It is also not included in the API, so it should either be included in it or this PR be applied.
\| \| \| * \|	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 #925: Document Extraction TestCompile	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
\|\ \ \ \ \ \ \ \ \
\| \| \| \| \| \| \| \| \| *	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
\| \| \| \| \| \| \| \|
\| \| \| \| \| \| * \|	Fix typo and Add Jason's example to the doc	Amin Timany	2017-07-31
\| \| \| \| \| \| \| \|
\| \| \| \| \| \| * \|	Improve documentation of cumulativity	Amin Timany	2017-07-31
\| \|_\|_\|_\|_\|/ / \|/\| \| \| \| \| \|
\| \| \| * \| \| \|	Drop paragraph mentioning Addendum as separate doc.	Théo Zimmermann	2017-07-29
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	As suggested by @herbelin.
* \| \| \| \| \| \|	Merge PR #823: Async off in Windows by default in CoqIDE	Maxime Dénès	2017-07-28
\|\ \ \ \ \ \ \
\| \| \| \| \| \| \| *	Fix some coq-tex errors in the reference manual.	Guillaume Melquiond	2017-07-28
\| \|_\|_\|_\|_\|_\|/ \|/\| \| \| \| \| \|
\| \| \| \| \| \| *	Fix documentation of Hint Mode (bug #4911).	Guillaume Melquiond	2017-07-28
\| \|_\|_\|_\|_\|/ \|/\| \| \| \| \|
\| \| \| \| \| *	Fix shuffled documentation.	Guillaume Melquiond	2017-07-28
\| \|_\|_\|_\|/ \|/\| \| \| \|
\| \| \| \| *	Add missing paragraph to introduction	Benjamin Pierce	2017-07-27
\| \|_\|_\|/ \|/\| \| \|
\| \| \| *	Extraction.tex: mention the possible "From Coq Require Extraction"	letouzey	2017-07-27
\| \| \| \|
\| \| \| *	Extraction TestCompile documented + mentionned in CHANGES	Pierre Letouzey	2017-07-27
\| \|_\|/ \|/\| \| \| \| \| \| \| \|	Also includes a minor fix of the Extraction doc (a Require was missing).
\| \| *	[toplevel] Remove long ago deprecated and NOOP options.	Emilio Jesus Gallego Arias	2017-07-27
\| \|/ \|/\| \| \| \| \|	Minor clean up, no sense in having these as they do nothing.
* \|	Adding a V8.7 compatibility version number.	Hugo Herbelin	2017-07-21
\| \|
* \|	Merge branch 'v8.7'	Maxime Dénès	2017-07-20
\|\ \
\| * \	Merge PR #745: Add timing scripts	Maxime Dénès	2017-07-19
\| \|\ \
* \| \ \	Merge PR #865: RefMan-ext: fix some typos	Maxime Dénès	2017-07-17
\|\ \ \ \
\| * \| \| \|	Update with non structurally recursive	william-lawvere	2017-07-14
\| \| \| \| \|
\| \| * \| \|	Sync the manual with the deprecation warnings.	Théo Zimmermann	2017-07-11
\| \|/ / / \|/\| \| \|
\| \| * \|	Document the timing targets	Jason Gross	2017-07-11
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	We document the most useful timing targets and variables, how to invoke them, and what the output looks like.
\| \| * \|	Strip trailing spaces	Jason Gross	2017-07-11
\| \|/ / \|/\| \|
\| * \|	RefMan-ext: fix some typos	William Lawvere	2017-07-07
\| \| \|
* \| \|	Merge PR #842: Update the Tutorial.	Maxime Dénès	2017-07-07
\|\ \ \
* \ \ \	Merge PR #835: Remove doc/refman/RefMan-ind.tex	Maxime Dénès	2017-07-07
\|\ \ \ \ \| \|_\|/ / \|/\| \| \|
* \| \| \|	Merge PR #837: Add inversion_sigma to CHANGES and to doc	Maxime Dénès	2017-07-05
\|\ \ \ \
* \ \ \ \	Merge PR #850: Improve grammar in RefMan-Gal and RefMan-syn	Maxime Dénès	2017-07-05
\|\ \ \ \ \
* \ \ \ \ \	Merge PR #832: Document an example `Makefile` for `coq_makefile`	Maxime Dénès	2017-07-05
\|\ \ \ \ \ \
* \ \ \ \ \ \	Merge branch 'v8.6'	Pierre-Marie Pédrot	2017-07-04
\|\ \ \ \ \ \ \
\| \| \| * \| \| \| \|	Update RefMan-syn.tex	william-lawvere	2017-07-01
\| \| \| \| \| \| \| \|
\| \| \| * \| \| \| \|	Merge remote-tracking branch 'upstream/trunk' into trunk	William Lawvere	2017-07-01
\| \| \| \|\ \ \ \ \ \| \|_\|_\|/ / / / / \|/\| \| \| \| \| \| \|
\| \| \| * \| \| \| \|	RefMan-gal: improve grammar	William Lawvere	2017-07-01
\| \| \| \| \| \| \| \|
\| \| \| * \| \| \| \|	RefMan-syn: grammar edit	William Lawvere	2017-07-01
\| \| \| \| \| \| \| \|
\| \| * \| \| \| \| \|	Document an example `Makefile` for `coq_makefile`	Jason Gross	2017-06-30
\| \|/ / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	We document an example `Makefile` which does not include the generated `CoqMakefile`, but instead invokes arbitrary targets in it.
\| \| \| \| * \| \|	Remove doc/refman/RefMan-ind.tex	Jason Gross	2017-06-30
\| \|_\|_\|/ / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	It does not seem to be referred to by any file, and does not seem to be built by any implicit rules.
\| \| \| * \| \|	Add doc for inversion_sigma to RefMan-tac	Jason Gross	2017-06-30
\| \|_\|/ / / \|/\| \| \| \|
\| \| \| * \|	Mention again how to report bug and get version number.	Théo Zimmermann	2017-06-30
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	As suggested by @psteckler.
\| \| \| * \|	Better phrasing.	Théo Zimmermann	2017-06-29
\| \| \| \| \|
\| \| \| * \|	More substance on discouraged practices.	Théo Zimmermann	2017-06-29
\| \| \| \| \|
\| \| \| * \|	Some more corrections to the tutorial.	Théo Zimmermann	2017-06-29
\| \| \| \| \|
\| \| \| * \|	Mask the reliance on coqtop.	Théo Zimmermann	2017-06-29
\| \| \| \| \|
\| \| \| * \|	Update the Tutorial.	Théo Zimmermann	2017-06-28
\| \|_\|/ / \|/\| \| \|