coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Unbreak RecTutorial.v	Gaëtan Gilbert	2017-08-01
\| \| \| \| \|	The RecTutorial.tex still contains similarly broken Coq code, it just doesn't run it.
*	Remove old doc/rt files.	Gaëtan Gilbert	2017-08-01
\|
*	Add dev/v8-syntax/check-grammar byproducts to gitignore.	Gaëtan Gilbert	2017-08-01
\|
*	Remove obsolete files	Gaëtan Gilbert	2017-08-01
\| \| \| \| \|	db_printers just isn't used. api.txt is superseded by the API OCaml interface.
*	Add .v extension to dev/doc/notes-on-conversion	Gaëtan Gilbert	2017-08-01
\| \| \| \|	This gives syntax highlighting in Coq-aware editors.
*	Remove dev/TODO	Gaëtan Gilbert	2017-08-01
\|
*	Fix syntax-v8.tex bad parenthesizing	Gaëtan Gilbert	2017-08-01
\| \| \| \|	Introduced c1e9a27d383688e44ba34ada24fe08151cb5846e
*	Remove unused Makefiles in dev/tools/	Gaëtan Gilbert	2017-08-01
\| \| \| \|	They seem unused since 8f4b7f1 (2007).
*	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
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #761: deprecate Pp.std_ppcmds type and promote Pp.t instead	Maxime Dénès	2017-07-31
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #746: Timing on ci via coq_makefile for various projects	Maxime Dénès	2017-07-31
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| * \| \|	Drop paragraph mentioning Addendum as separate doc.	Théo Zimmermann	2017-07-29
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	As suggested by @herbelin.
\| \| \| \| * \| \| \| \| \| \| \| \| \| \| \| \| \|	closing bug 5315	Julien Forest	2017-07-29
\| \|_\|_\|/ / / / / / / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Merge PR #923: [api] Fix base_include LTAC parts.	Maxime Dénès	2017-07-28
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #889: Removing template polymorphism for definitions.	Maxime Dénès	2017-07-28
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #888: Stronger kernel types	Maxime Dénès	2017-07-28
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #823: Async off in Windows by default in CoqIDE	Maxime Dénès	2017-07-28
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #782: Update API for fiat	Maxime Dénès	2017-07-28
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| *	Fix documentation of Hint Mode (bug #4911).	Guillaume Melquiond	2017-07-28
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| * \|	Fix shuffled documentation.	Guillaume Melquiond	2017-07-28
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|/
* \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Merge PR #852: Makefile: fails if some .vo or .cm* file has no source	Maxime Dénès	2017-07-28
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| * \|	Add missing paragraph to introduction	Benjamin Pierce	2017-07-27
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|/
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| * /	Fixing bug #5671 (specialize unclean wrt Metas).	Hugo Herbelin	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).
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| * \|	test-suite: more use of the new command Extraction TestCompile	Pierre Letouzey	2017-07-27
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| * \| \| \| \| \| \| \| \| \|	[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.
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| * \|	[make] remove compat5 file.	Emilio Jesus Gallego Arias	2017-07-27
\| \| \| \| \| \| \| \| \| \| \|_\|_\|_\|_\|_\|/ / \| \| \| \| \| \| \| \| \| \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	It is empty and not used anymore.
\| \| \| \| \| \| * \| \| / \| \| \| \| \| \| \|	[api] Fix base_include LTAC parts.	Emilio Jesus Gallego Arias	2017-07-27
\| \| \| \| \| \| \| \|_\|/ / / / / / / / \| \| \| \| \| \| \|/\| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| * \| \| \| \| \| \| \|	deprecate Pp.std_ppcmds type alias	Matej Košík	2017-07-27
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| * \| \| \| \| \| \| \| \| \|	Fix TypeclassDebug.out after conflicting PR merges	Matthieu Sozeau	2017-07-26
\| \|_\|_\|_\|_\|/ / / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| \| \| \| \| \| *	test-suite/success/extraction.v : add some Extraction TestCompile	Pierre Letouzey	2017-07-26
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| \| \| \| \| \| *	Enrich test file 4720.v with a compilation test of the extracted code	Pierre Letouzey	2017-07-26
\| \|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|/ \|/\| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| \| * \| \| \|	adding a test-suite file 4709.v (thanks to the new command Extraction ↵	Pierre Letouzey	2017-07-26
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	TestCompile)
\| \| \| \| \| \| \| \| \| \| * \| \| \|	Extraction: reduce primitive projections in types (fix bug 4709)	Pierre Letouzey	2017-07-26
\| \|_\|_\|_\|_\|_\|_\|_\|_\|/ / / / \|/\| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| \| \| \| *	Remove a few useless evar-normalizations in printing code.	Pierre-Marie Pédrot	2017-07-26
\| \|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|/ \|/\| \| \| \| \| \| \| \| \| \| \|