coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Removing a redundant universe instance information in native compute.	Pierre-Marie Pédrot	2017-07-10
\| \| \| \| \| \|	Global declarations used to carry universe instances with them, but it turns out this information is not used anywhere. Instead, instances were already properly encoded as the first argument of polymorphic definitions.
*	Merge PR #853: Clean 'with Definition' implementation.	Maxime Dénès	2017-07-06
\|\
* \	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 #840: Quote $(OCAMLFIND) in CoqMakefile.in for Windows	Maxime Dénès	2017-07-05
\|\ \ \ \
* \ \ \ \	Merge PR #839: Update .gitignore with doc/tutorial/Tutorial.v.out	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
\|\ \ \ \ \ \ \
* \| \| \| \| \| \| \|	Bump year in headers.	Pierre-Marie Pédrot	2017-07-04
\| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| *	Removing dead code in Subtyping.	Pierre-Marie Pédrot	2017-07-04
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	This code was a sketch of what to do when we properly implement module-level handling of instanciation of definitions by inductive types. It was completely dead code, called after an error, and somewhat incorrect. Instead of letting it bitrot, we remove it.
\| \| \| \| \| \| \| *	Removing a few suspicious functions from the kernel.	Pierre-Marie Pédrot	2017-07-03
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	These functions were messing with the deferred universe constraints in an error-prone way, and were only used for printing as of today. We inline the one used by the printer instead.
\| \| \| \| \| \| \| *	Do not add original constraints to the environment in 'with Definition' check.	Pierre-Marie Pédrot	2017-07-03
\| \|_\|_\|_\|_\|_\|/ \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	This was useless, because immediate constraints are assumed to already be in the current environment, while deferred constraints are useless for the conversion check of the definition types, as they only appear in the opaque body. This also clarifies a bit what is going on in the typing of module constraints w.r.t. global universes.
\| \| \| \| \| * \|	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.
\| \| \| \| \| *	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)
* \| \|	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
\|\ \ \ \
\| \| * \| \|	Fix OS X Travis by pinning OCaml version.	Théo Zimmermann	2017-06-30
\| \|/ / / \|/\| \| \|
\| * \| \|	closing bug #5618 introduce by PR 828	Julien Forest	2017-06-29
\| \| \| \|
* \| \| \|	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.