coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Getting rid of pf_is_matching in Funind.	Pierre-Marie Pédrot	2017-12-06
*	Merge PR #890: Global universe declarations	Maxime Dénès	2017-12-05
\|\
* \	Merge PR #6266: Safe unmarshalling in the checker	Maxime Dénès	2017-12-05
\|\ \
* \ \	Merge PR #6301: [vernac] Couple of tweaks missing from previous PRs.	Maxime Dénès	2017-12-05
\|\ \ \
* \ \ \	Merge PR #6306: Adding a test for #6304 (a bug with "fix" in notations).	Maxime Dénès	2017-12-05
\|\ \ \ \
* \ \ \ \	Merge PR #6300: Clarify operation of sequences, fixes #6095	Maxime Dénès	2017-12-05
\|\ \ \ \ \
* \ \ \ \ \	Merge PR #6220: Use OCaml criteria for infix ops in extraction, #6212	Maxime Dénès	2017-12-05
\|\ \ \ \ \ \
* \ \ \ \ \ \	Merge PR #6293: Check for Num lib if OCaml >= 4.06, fixes #6162	Maxime Dénès	2017-12-05
\|\ \ \ \ \ \ \
* \ \ \ \ \ \ \	Merge PR #6302: Uninstall doc dir, not dev (which is not installed), fixes #6007	Maxime Dénès	2017-12-05
\|\ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \	Merge PR #6287: Add merlin to default.nix	Maxime Dénès	2017-12-05
\|\ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \	Merge PR #6210: More complete not-fully-applied error messages, #6145	Maxime Dénès	2017-12-05
\|\ \ \ \ \ \ \ \ \ \
\| \| \| \| \| \| \| \| * \| \|	[vernac] Couple of tweaks missing from previous PRs.	Emilio Jesus Gallego Arias	2017-12-04
\| \|_\|_\|_\|_\|_\|_\|/ / / \|/\| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| * \| \|	Adding a test for #6304 (bug with fix in notations).	Hugo Herbelin	2017-12-03
\| \|_\|_\|_\|_\|_\|/ / / \|/\| \| \| \| \| \| \| \|
\| \| \| * \| \| \| \| \|	uninstall doc dir, not dev (which is not installed), #6007	Paul Steckler	2017-12-01
\| \|_\|/ / / / / / \|/\| \| \| \| \| \| \|
\| \| \| * \| \| \| \|	check for Num lib if OCaml >= 4.06, #6162	Paul Steckler	2017-12-01
\| \| \| \| \| * \| \|	clarify operation of sequences, #6095	Paul Steckler	2017-12-01
\| \| \| \| \|/ / / \| \| \| \|/\| \| \|
\| \| \| \| \| \| *	Update CHANGES	Matthieu Sozeau	2017-12-01
\| \| \| \| \| \| *	Cleanup API for registering universe binders.	Matthieu Sozeau	2017-12-01
\| \| \| \| \| \| *	[refman] Expand a little on global universes.	Matthieu Sozeau	2017-12-01
\| \| \| \| \| \| *	Tests for global universe declarations	Matthieu Sozeau	2017-12-01
\| \| \| \| \| \| *	Proper nametab handling of global universe names	Matthieu Sozeau	2017-12-01
\| \|_\|_\|_\|_\|/ \|/\| \| \| \| \|
* \| \| \| \| \|	Merge PR #736: [ci] Test coqchk on the CompCert target.	Maxime Dénès	2017-12-01
\|\ \ \ \ \ \
* \ \ \ \ \ \	Merge PR #6256: CI: better ocaml warning checks	Maxime Dénès	2017-12-01
\|\ \ \ \ \ \ \
* \ \ \ \ \ \ \	Merge PR #6276: Coqchk accepts filenames	Maxime Dénès	2017-12-01
\|\ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \	Merge PR #6233: [proof] [api] Rename proof types in preparation for functiona...	Maxime Dénès	2017-12-01
\|\ \ \ \ \ \ \ \ \ \| \|_\|_\|_\|_\|_\|/ / / \|/\| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \|	Merge PR #1049: Remove obsolete locality	Maxime Dénès	2017-11-30
\|\ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \	Merge PR #6244: [lib] [api] Introduce record for `object_prefix`	Maxime Dénès	2017-11-30
\|\ \ \ \ \ \ \ \ \ \
\| \| \| \| \| \| * \| \| \| \|	[ci] Test coqchk on the CompCert target.	Théo Zimmermann	2017-11-30
* \| \| \| \| \| \| \| \| \| \|	Merge PR #6274: Attempt to fix inversion disregarding singleton types (fixes ...	Maxime Dénès	2017-11-30
\|\ \ \ \ \ \ \ \ \ \ \ \| \|_\|_\|_\|_\|_\|/ / / / / \|/\| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| * \| \|	Add merlin in the dependencies of nix-shell only.	Théo Zimmermann	2017-11-30
\| \|_\|_\|_\|_\|_\|_\|/ / / \|/\| \| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \| \|	Merge PR #6269: [ci] [vst] Shorten compilation time to avoid Travis timeouts.	Maxime Dénès	2017-11-30
\|\ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \	Merge PR #6193: Fix (partial) #4878: option to stop autodeclaring axiom as in...	Maxime Dénès	2017-11-30
\|\ \ \ \ \ \ \ \ \ \ \
\| \| \| \| \| * \| \| \| \| \| \|	Remove "obsolete_locality" and fix STM vernac classification.	Maxime Dénès	2017-11-29
\| \|_\|_\|_\|/ / / / / / / \|/\| \| \| \| \| \| \| \| \| \|
\| \| \| \| * \| \| \| \| \| \|	[lib] [api] Introduce record for `object_prefix`	Emilio Jesus Gallego Arias	2017-11-29
\| \| \| \| \| * \| \| \| \| \|	[proof] [api] Rename proof types in preparation for functionalization.	Emilio Jesus Gallego Arias	2017-11-29
\| \|_\|_\|_\|/ / / / / / \|/\| \| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \| \|	Merge PR #6271: Add PR backport script.	Maxime Dénès	2017-11-29
\|\ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \	Merge PR #6253: Fixing inconsistent associativity of level 10 in the table of...	Maxime Dénès	2017-11-29
\|\ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \	Merge PR #6199: [vernac] Uniformize type of vernac interpretation.	Maxime Dénès	2017-11-29
\|\ \ \ \ \ \ \ \ \ \ \ \
\| \| \| \| \| \| \| \| * \| \| \| \|	coq_makefile: pass filenames to coqchk	Ralf Jung	2017-11-29
\| \| \| \| \| \| \| \| * \| \| \| \|	Documenting the possibility to pass filenames to coqchk.	Pierre-Marie Pédrot	2017-11-29
\| \| \| \| \| \| \| \| * \| \| \| \|	Allow to pass physical files to coqchk.	Pierre-Marie Pédrot	2017-11-29
\| \| \| \| \| \| * \| \| \| \| \| \|	In injection/inversion, consider all template-polymorphic types as injectable.	Hugo Herbelin	2017-11-28
\| \| \| \| \| \| \| \| \| \| \| * \|	use \ocaml macro in new text	Paul Steckler	2017-11-28
\| \| \| \| \| \| * \| \| \| \| \| \|	Adding a variant get_truncation_family_of of get_sort_family_of.	Hugo Herbelin	2017-11-28
\| \| \| \| \| \| * \| \| \| \| \| \|	Moving non-recursive function sort_family_of out of the retype block of recur...	Hugo Herbelin	2017-11-28
\| \| \| \| \| \| \|/ / / / / /
\| \| \| \| \| \| \| * / / / /	Adding an interface file for checker/check.ml.	Pierre-Marie Pédrot	2017-11-28
\| \|_\|_\|_\|_\|_\|/ / / / / \|/\| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| * \| \|	more complete not-fully-applied error messages, #6145	Paul Steckler	2017-11-28
\| \| \| * \| \| \| \| \| \| \|	Add PR backport script.	Théo Zimmermann	2017-11-28
\| \|_\|/ / / / / / / / \|/\| \| \| \| \| \| \| \| \|
\| \| \| \| * \| \| \| \| \|	[ci] [vst] Shorten compilation time to avoid Travis timeouts.	Emilio Jesus Gallego Arias	2017-11-28
\| \|_\|_\|/ / / / / / \|/\| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| *	Use safe demarshalling in the checker.	Pierre-Marie Pédrot	2017-11-28