coq - The formal proof system

Age	Commit message (Collapse)	Author
2017-08-12	Merge PR #963: fix coq_makefile	Maxime Dénès

2017-08-12	fix coq_makefile	Matej Košík
	Make sure that when plugin writer does not use -bypass-API, API is opened by default.
2017-08-02	Makefile: 'make clean' now immune to the check for binary files without sources	Pierre Letouzey
	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).
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 #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
	y , z".
2017-08-01	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-07-31	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-29	Drop paragraph mentioning Addendum as separate doc.	Théo Zimmermann
	As suggested by @herbelin.
2017-07-29	closing bug 5315	Julien Forest

2017-07-28	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-27	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
	Also includes a minor fix of the Extraction doc (a Require was missing).
2017-07-27	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
	Minor clean up, no sense in having these as they do nothing.
2017-07-27	[make] remove compat5 file.	Emilio Jesus Gallego Arias
	It is empty and not used anymore.
2017-07-27	[api] Fix base_include LTAC parts.	Emilio Jesus Gallego Arias

2017-07-27	deprecate Pp.std_ppcmds type alias	Matej Košík

2017-07-26	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
	TestCompile)
2017-07-26	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	Add a comment regarding the specialization of the combinator in Detyping.	Pierre-Marie Pédrot

2017-07-26	Merge PR #918: Extraction: do not mix Haskell types Any and () (fix bugs ↵	Maxime Dénès
	4844 and 4824)
2017-07-26	Merge PR #910: Add [opam update] and online repository to gitlab CI script.	Maxime Dénès

2017-07-26	Removing default evar-normalization for ARGUMENT EXTEND.	Pierre-Marie Pédrot
	This fixes bug 5650: evar (x : Prop) should not be slow.
2017-07-26	Merge PR #886: Fixing what was presumably a typo in the naming conventions file	Maxime Dénès