coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
\| \| * \| \| \| \| \| \|	Safe API for accessing universe constraints of global references.	Pierre-Marie Pédrot	2017-07-11
\| \| * \| \| \| \| \| \|	Less footguns in universe handling: remove subst_instance_context.	Pierre-Marie Pédrot	2017-07-11
\| \| * \| \| \| \| \| \|	Asserting that monomorphic section variables have no abstracted context.	Pierre-Marie Pédrot	2017-07-11
\| \| * \| \| \| \| \| \|	Getting rid of simple calls to AUContext.instance.	Pierre-Marie Pédrot	2017-07-11
\| \|/ / / / / / /
* \| \| \| \| \| \| \|	Merge branch 'v8.7'	Maxime Dénès	2017-07-11
\|\ \ \ \ \ \ \ \ \| \|/ / / / / / / \|/\| \| \| \| \| \| \|
\| * \| \| \| \| \| \|	Merge PR #858: [travis] Remove CompCert version check hack.	Maxime Dénès	2017-07-11
\| \|\ \ \ \ \ \ \
* \| \ \ \ \ \ \ \	Merge PR #867: Removing a redundant universe instance information in native c...	Maxime Dénès	2017-07-11
\|\ \ \ \ \ \ \ \ \
\| \| * \ \ \ \ \ \ \	Merge PR #860: use Int.equal instead of polymorphic =	Maxime Dénès	2017-07-11
\| \| \|\ \ \ \ \ \ \ \
\| * \| \| \| \| \| \| \| \| \|	Removing a redundant universe instance information in native compute.	Pierre-Marie Pédrot	2017-07-10
\|/ / / / / / / / / /
\| \| \| \| * \| \| \| \| \|	Adding support for bindings tags to explicit prefix/suffix rather than colors.	Hugo Herbelin	2017-07-08
\| \| \| \| \| * \| \| \| \|	RefMan-ext: fix some typos	William Lawvere	2017-07-07
\| \|_\|_\|_\|/ / / / / \|/\| \| \| \| \| \| \| \|
\| * \| \| \| \| \| \| \|	Merge PR #863: Fixing environment in warning "Projection value has no head co...	Maxime Dénès	2017-07-07
\| \|\ \ \ \ \ \ \ \
\| * \ \ \ \ \ \ \ \	Merge PR #842: Update the Tutorial.	Maxime Dénès	2017-07-07
\| \|\ \ \ \ \ \ \ \ \
\| * \ \ \ \ \ \ \ \ \	Merge PR #816: In enter_one, not having exactly one goal is a fatal error of ...	Maxime Dénès	2017-07-07
\| \|\ \ \ \ \ \ \ \ \ \
\| * \ \ \ \ \ \ \ \ \ \	Merge PR #835: Remove doc/refman/RefMan-ind.tex	Maxime Dénès	2017-07-07
\| \|\ \ \ \ \ \ \ \ \ \ \
\| * \| \| \| \| \| \| \| \| \| \| \|	Set version to 8.7.0~alpha.	Maxime Dénès	2017-07-07
\| * \| \| \| \| \| \| \| \| \| \| \|	Merge PR #844: Better support for make TIMED=1 on Windows	Maxime Dénès	2017-07-07
\| \|\ \ \ \ \ \ \ \ \ \ \ \
\| * \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #800: Enable fiat-crypto	Maxime Dénès	2017-07-07
\| \|\ \ \ \ \ \ \ \ \ \ \ \ \
\| \| \| \| \| \| \| * \| \| \| \| \| \| \|	Fixing environment in warning "Projection value has no head constant".	Hugo Herbelin	2017-07-07
* \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Merge PR #853: Clean 'with Definition' implementation.	Maxime Dénès	2017-07-06
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \| \|/ / / / / / / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| * \| \| \| \| \| \|	use Int.equal instead of polymorphic =	Paul Steckler	2017-07-05
\| \| \| \| \| \| \| \| \| \|/ / / / / \| \| \| \| \| \| \| \| \|/\| \| \| \| \|
\| \| \| \| \| \| \| \| \| * \| \| \| \|	[travis] Remove CompCert version check hack.	Emilio Jesus Gallego Arias	2017-07-05
\| \| \| \| \| \| \| \| \|/ / / / /
* \| \| \| \| \| \| \| \| \| \| \| \|	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
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
\| \| \| \| \| \| \| * \| \| \| \| \| \| \| \| \|	Revert fiat-crypto overlay	Jason Gross	2017-07-04
\| \|_\|_\|_\|_\|_\|/ / / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	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
\| \| \| \| \| \| \| * \| \| \| \| \| \| \| \|	Removing a few suspicious functions from the kernel.	Pierre-Marie Pédrot	2017-07-03
\| \| \| \| \| \| \| * \| \| \| \| \| \| \| \|	Do not add original constraints to the environment in 'with Definition' check.	Pierre-Marie Pédrot	2017-07-03
\| \|_\|_\|_\|_\|_\|/ / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| * \| \| \| \| \| \| \| \| \|	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
\| \|/ / / / / / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| * \| \| \| \| \| \|	Remove doc/refman/RefMan-ind.tex	Jason Gross	2017-06-30
\| \|_\|_\|_\|_\|_\|/ / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| * \| \| \| \| \| \| \|	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
\| \| * \| \| \| \| \| \| \| \|	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
\| \|/ / / / / / / / / \|/\| \| \| \| \| \| \| \| \|
\| \| \| * \| \| \| \| \| \|	Better support for make TIMED=1 on Windows	Jason Gross	2017-06-30
\| \|_\|/ / / / / / / \|/\| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \|	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