coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Merge PR #873: New strategy based on open scopes for deciding which notation ...	Maxime Dénès	2017-12-07
\|\
* \	Merge PR #6142: Single quotes break on Windows	Maxime Dénès	2017-12-07
\|\ \
* \ \	Merge PR #6277: Qualified import in coqchk	Maxime Dénès	2017-12-07
\|\ \ \
* \ \ \	Merge PR #6322: Fix #6286 (non stability of micromega csdp cache rebuilding)	Maxime Dénès	2017-12-07
\|\ \ \ \
* \ \ \ \	Merge PR #6321: Use preference for ocamlfind in configure	Maxime Dénès	2017-12-07
\|\ \ \ \ \
* \ \ \ \ \	Merge PR #6316: Correct typo	Maxime Dénès	2017-12-07
\|\ \ \ \ \ \
* \ \ \ \ \ \	Merge PR #6309: [default.nix] needs ncurses for the test-suite	Maxime Dénès	2017-12-07
\|\ \ \ \ \ \ \
* \ \ \ \ \ \ \	Merge PR #6303: Remove redundant Zcase from the checker.	Maxime Dénès	2017-12-07
\|\ \ \ \ \ \ \ \
\| \| \| \| \| * \| \| \|	Replacing Hashtbl.add by Hashtbl.replace in micromega cache building.	Hugo Herbelin	2017-12-05
\| \| \| \| * \| \| \| \|	use preference for ocamlfind	Paul Steckler	2017-12-05
\| \|_\|_\|/ / / / / \|/\| \| \| \| \| \| \|
\| \| \| * \| \| \| \|	Correct typo	Martin Vassor	2017-12-05
\| \|_\|/ / / / / \|/\| \| \| \| \| \|
\| \| * \| \| \| \|	[default.nix] explain ncurses dependency	Vincent Laporte	2017-12-05
* \| \| \| \| \| \|	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
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \| \|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|/ / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| \| \| \| * \| \| \|	[default.nix] needs ncurses for the test-suite	Vincent Laporte	2017-12-04
\| \|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|/ / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| * \| \| \| \| \| \|	[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
\| \|_\|_\|_\|_\|_\|/ / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| * \| \| \|	Remove redundant Zcase from the checker.	Pierre-Marie Pédrot	2017-12-02
\| \|_\|_\|_\|_\|_\|_\|_\|/ / / / \|/\| \| \| \| \| \| \| \| \| \| \|
\| \| \| * \| \| \| \| \| \| \| \|	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
\| \|_\|_\|_\|_\|/ / / / \|/\| \| \| \| \| \| \| \|
\| \| \| \| \| \| * \| \|	Documenting the -Q flag of coqchk.	Pierre-Marie Pédrot	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
\| \| \| \| \| \| \| \| \| \| \| * \| \|	Forbid implicitly relative names in the checker.	Pierre-Marie Pédrot	2017-11-29
\| \| \| \| \| \| \| \| \| \| \| * \| \|	Mark the -I option in coqchk as deprecated and merge it with -Q.	Pierre-Marie Pédrot	2017-11-29