coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
...
\| \| * \| \| \| \| \| \| \| \|	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
\| \| \| \| \| \| \| \| \|
\| \| \| \| \| * \| \| \|	Update CHANGES with inversion_sigma entry	Jason Gross	2017-06-30
\| \|_\|_\|_\|/ / / / \|/\| \| \| \| \| \| \|
\| \| * \| \| \| \| \|	Update .gitignore with doc/tutorial/Tutorial.v.out	Jason Gross	2017-06-30
\| \|/ / / / / / \|/\| \| \| \| \| \|
\| \| * \| \| \| \|	Fix more potential quoting issues: COQBIN , COQLIB	Jason Gross	2017-06-30
\| \| \| \| \| \| \|
\| \| * \| \| \| \|	Also quote $(COQLIB)/grammar	Jason Gross	2017-06-30
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	In case COQLIB has backslashes, as it does on Windows, or spaces
\| \| * \| \| \| \|	Create a variable for CAMLDOC in CoqMakefile.in	Jason Gross	2017-06-30
\| \| \| \| \| \| \|
\| \| * \| \| \| \|	Quote $(OCAMLFIND) in CoqMakefile.in for Windows	Jason Gross	2017-06-30
\| \|/ / / / / \|/\| \| \| \| \| \| \| \| \| \| \|	This, I hope, will fix [bug #5620](https://coq.inria.fr/bugs/show_bug.cgi?id=5620)
\| \| \| * \| \|	Better support for make TIMED=1 on Windows	Jason Gross	2017-06-30
\| \|_\|/ / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \|	This fixes [bug #5619](https://coq.inria.fr/bugs/show_bug.cgi?id=5619)
* \| \| \| \|	Merge PR#846: Fix OS X Travis by pinning OCaml version.	Maxime Dénès	2017-06-30
\|\ \ \ \ \
* \ \ \ \ \	Merge PR#843: closing bug #5618 introduce by PR 828	Maxime Dénès	2017-06-30
\|\ \ \ \ \ \
\| \| \| \| \| \| *	Mention again how to report bug and get version number.	Théo Zimmermann	2017-06-30
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	As suggested by @psteckler.
\| \| * \| \| \| \|	Fix OS X Travis by pinning OCaml version.	Théo Zimmermann	2017-06-30
\| \|/ / / / / \|/\| \| \| \| \|
\| \| \| \| \| *	Better phrasing.	Théo Zimmermann	2017-06-29
\| \| \| \| \| \|
\| \| \| \| \| *	More substance on discouraged practices.	Théo Zimmermann	2017-06-29
\| \| \| \| \| \|
\| * \| \| \| \|	closing bug #5618 introduce by PR 828	Julien Forest	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
\| \| \| \| \| \|
* \| \| \| \| \|	Merge PR#810: An attempt to fix a failure of test deps-checksum.sh fails ↵	Maxime Dénès	2017-06-27
\|\ \ \ \ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	with make -j4
\| \| \| * \ \ \	Merge PR#731: Mini-cleaning around OCaml file names	Maxime Dénès	2017-06-27
\| \| \| \|\ \ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	This is only a partial merge, we stick with using the standard OCaml (un)capitalize functions.
\| \| \| \| * \| \| \|	A cleaning phase about ocaml file names.	Hugo Herbelin	2017-06-27
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Ocaml file names are restricted since 2008 to A..Z followed by a..z0..9'_. We take this constraint into account in tools manipulating Ocaml file names.
\| \| \| * \| \| \| \|	Merge PR#814: Fix #5380: Default colors for CoqIDE are actually applied.	Maxime Dénès	2017-06-27
\| \| \| \|\ \ \ \ \
* \| \| \| \ \ \ \ \	Merge PR#826: Put plugin exports in the right compatibility file	Maxime Dénès	2017-06-26
\|\ \ \ \ \ \ \ \ \ \| \|_\|_\|_\|_\|_\|_\|_\|/ \|/\| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \|	Merge PR#825: Ignore all PDF files.	Maxime Dénès	2017-06-26
\|\ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \	Merge PR#828: closing bug #4250	Maxime Dénès	2017-06-26
\|\ \ \ \ \ \ \ \ \ \ \| \| \|_\|_\|/ / / / / / \| \|/\| \| \| \| \| \| \| \|
\| \| \| \| \| * \| \| \| \|	Bump version number to 8.6.1.	Maxime Dénès	2017-06-26
\| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| * \| \| \| \|	Fix libpcre dependency issue under Windows.	Maxime Dénès	2017-06-26
\| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| * \| \| \| \|	Fix proxy setting issue	Michael Soegtrop	2017-06-26
\| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| * \| \| \| \|	Fixes bug #5561,#5562 in Windows build system	Michael Soegtrop	2017-06-26
\| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| * \| \| \| \|	Merge PR#756: Fix Bug #5574, document function scope	Maxime Dénès	2017-06-26
\| \| \| \| \| \|\ \ \ \ \
* \| \| \| \| \| \ \ \ \ \	Merge PR#824: Fix printers	Maxime Dénès	2017-06-23
\|\ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \	Merge PR#821: [vernac] Remove stale bool parameter from ↵	Maxime Dénès	2017-06-23
\|\ \ \ \ \ \ \ \ \ \ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	`VernacStartTheoremProof`
* \ \ \ \ \ \ \ \ \ \ \ \	Merge PR#820: [ide] Correct more merging errors.	Maxime Dénès	2017-06-23
\|\ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR#815: STM: par: report no error to UIs in non-solve mode	Maxime Dénès	2017-06-23
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR#794: Cleanup of ltac cmxs	Maxime Dénès	2017-06-23
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR#762: [vernac] Fix unneeded mutual references in Obligations	Maxime Dénès	2017-06-23
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
\| \| \| \| \| \| \| \| \| \| \| * \ \ \ \ \	Merge PR#813: Fix plugin warnings	Maxime Dénès	2017-06-23
\| \| \| \| \| \| \| \| \| \| \| \|\ \ \ \ \ \
\| \| \| \| \| \| \| \| \| \| \| \| \| * \| \| \| \|	Fix Bug #5574, document function scope	Paul Steckler	2017-06-23
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \|/ / / \| \| \| \| \| \| \| \| \| \| \| \| \| \|/\| \| \|
\| \| \| \| \| \| \| * \| \| \| \| \| / \| \| \|	closing bug #4250	Julien Forest	2017-06-23
\| \|_\|_\|_\|_\|_\|/ / / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| \| * \| \| \| \| \|	[configure] 'ocaml' is more precise than OCaml as we mean the binary.	Maxime Dénès	2017-06-23
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Fix suggested by Hugo.
\| \| \| \| \| \| \| \| \| \| * \| \| \| \| \|	ocaml -> OCaml in configure.ml.	Maxime Dénès	2017-06-23
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| \| * \| \| \| \| \|	Merge PR#729: Fixing an inconsistency between configure and configure.ml	Maxime Dénès	2017-06-23
\| \| \| \| \| \| \| \| \| \| \|\ \ \ \ \ \
\| \| \| \| \| \| \| \| \| \| * \ \ \ \ \ \	Merge PR#740: Refactor documentation of records.	Maxime Dénès	2017-06-23
\| \| \| \| \| \| \| \| \| \| \|\ \ \ \ \ \ \
\| \| \| \| \| \| \| \| \| \| \| \| \| * \| \| \| \|	Add tests for handling of warnings	Tej Chajed	2017-06-23
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| \| \| \| \| * \| \| \| \|	Fix bug 5392: Warnings defined in plugins are considered unknown	Maxime Dénès	2017-06-23
\| \| \| \| \| \| \| \| \| \| \| \|_\|/ / / / / \| \| \| \| \| \| \| \| \| \| \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	The status of a warning can now be set before the warning is declared (typically by a plugin). However, I had to remove the "unknown warning" warning.
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| *	In enter_one, not having exactly one goal is a fatal error of the monad.	Hugo Herbelin	2017-06-23
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Pointed out by PMP.
\| \| \| \| \| \| \| \| * \| \| \| \| \| \| \| \|	Add test-suite file for funind, extraction with compat 8.6	Jason Gross	2017-06-22
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| * \| \| \| \| \| \| \| \|	Put plugin exports in the right compatibility file	Jason Gross	2017-06-22
\| \|_\|_\|_\|_\|_\|_\|/ / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	This closes [bug #5607](https://coq.inria.fr/bugs/show_bug.cgi?id=5607). PR #220 put the exports in the wrong compat files, presumably because it was originally targeted to version 8.6, and this wasn't updated when it was retargeted to version 8.7.