coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Merge PR #993: Credits for version 8.7	Maxime Dénès	2017-08-31
\|\
\| *	Credits for version 8.7	Matthieu Sozeau	2017-08-31
* \|	Merge PR #958: coq_makefile: build/use .cma for packed plugins too	Maxime Dénès	2017-08-31
\|\ \
\| * \|	coq_makefile: improve documentation	Enrico Tassi	2017-08-29
* \| \|	Merge PR #950: Rudimentary support for native_compute profiling, BZ#5170	Maxime Dénès	2017-08-29
\|\ \ \
* \ \ \	Merge PR #988: Fix obsolete description of real numerals.	Maxime Dénès	2017-08-29
\|\ \ \ \
* \ \ \ \	Merge PR #819: Cleanup old things	Maxime Dénès	2017-08-29
\|\ \ \ \ \
* \ \ \ \ \	Merge PR #773: [flags] Remove XML output flag.	Maxime Dénès	2017-08-29
\|\ \ \ \ \ \ \| \|_\|_\|_\|/ / \|/\| \| \| \| \|
\| \| \| \| \| *	Update coypright dates on documentation	Matthieu Sozeau	2017-08-23
\| \|_\|_\|_\|/ \|/\| \| \| \|
\| \| \| * \|	Fix obsolete description of real numerals.	Guillaume Melquiond	2017-08-22
\| \|_\|/ / \|/\| \| \|
\| \| \| *	use OCaml temp_file, instead of our own version	Paul Steckler	2017-08-18
* \| \| \|	Merge PR #973: Adding documentation for Printing Focused option.	Maxime Dénès	2017-08-18
\|\ \ \ \
\| \| \| \| *	Add native compute profiling, BZ#5170	Paul Steckler	2017-08-17
\| \|_\|_\|/ \|/\| \| \|
* \| \| \|	Merge PR #974: Change section caption, improve some wording	Maxime Dénès	2017-08-17
\|\ \ \ \
* \| \| \| \|	Document anonymous universes (PR #544).	Gaëtan Gilbert	2017-08-17
\| \| * \| \|	Adding documentation for Printing Focused option.	Pierre Courtieu	2017-08-17
\| \|/ / / \|/\| \| \|
\| * \| \|	mention that tactic is the identity or gives error	Paul Steckler	2017-08-16
\| * \| \|	change section caption, improve some wording	Paul Steckler	2017-08-16
\|/ / /
* \| \|	Merge PR #831: Port ssreflect user manual to Coq's latex/hevea style	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 #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 #864: Some cleanups after cumulativity for inductive types	Maxime Dénès	2017-08-16
\|\ \ \ \ \ \ \ \
\| \| \| \| \| \| * \| \|	Rewording the introduction	Enrico Tassi	2017-08-02
\| \| \| \| \| \| * \| \|	Rephrasing a couple of sentences in a more factual way.	Hugo Herbelin	2017-08-02
\| \| \| \| \| \| * \| \|	Rephrasing the introduction in a more factual and up-to-date way.	Hugo Herbelin	2017-08-02
\| \| \| \| \| \| * \| \|	Port ssr manual to Coq's latex/hevea style	Enrico Tassi	2017-08-02
\| \| \| \| \| \| * \| \|	Makefile.doc: implement serve-refman-8080 target	Enrico Tassi	2017-08-02
\| \|_\|_\|_\|_\|/ / / \|/\| \| \| \| \| \| \|
\| \| \| \| \| * \| \|	Update Setoid.tex	larsr	2017-08-02
\| \|_\|_\|_\|/ / / \|/\| \| \| \| \| \|
\| * \| \| \| \| \|	Typo in the documentation of cumulativity	Amin Timany	2017-08-02
\| \| \| \| \| \| *	Unbreak RecTutorial.v	Gaëtan Gilbert	2017-08-01
\| \| \| \| \| \| *	Remove old doc/rt files.	Gaëtan Gilbert	2017-08-01
\| \|_\|_\|_\|_\|/ \|/\| \| \| \| \|
\| \| \| \| \| *	[flags] Remove XML output flag.	Emilio Jesus Gallego Arias	2017-08-01
\| \|_\|_\|_\|/ \|/\| \| \| \|
\| \| \| * \|	Improve style slightly	Sam Pablo Kuper	2017-08-01
* \| \| \| \|	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
\| \|_\|_\|_\|_\|_\|_\|/ \|/\| \| \| \| \| \| \|
\| \| \| \| \| \| * \|	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
* \| \| \| \| \| \|	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
\| \|_\|_\|_\|_\|/ \|/\| \| \| \| \|