coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
\| \| \| \| \| \| \| \| \| \| \| \| * \| \| \| \| \| \| \| \|	[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
\| \|_\|_\|_\|/ / / / / / / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| \| \| \| \| \| * \| \| \|	Fix usage comment.	Théo Zimmermann	2017-11-29
\| \| \| \| \| \| \| \| \| \| \| \| \| \| * \| \| \|	This script apparently uses bash-specific features.	Théo Zimmermann	2017-11-29
\| \| \| \| \| \| \| \| \| \| \| \| \| \| * \| \| \|	Fix PR merge script.	Théo Zimmermann	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
\| \| \| \| \| \| \| \| \| \| \| * \| \| \| \|	Add a -Q option to coqchck.	Pierre-Marie Pédrot	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
\| \| \| \| \| \| \| \| * \| \| \| \|	Use large arrays in the checker demarshaller.	Pierre-Marie Pédrot	2017-11-28
\| \|_\|_\|_\|_\|_\|_\|/ / / / / \|/\| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| * \| \| \| \| \| \|	CI: use -byte-only in [warnings] jobs.	Gaëtan Gilbert	2017-11-28