coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
\| \| * \| \| \| \|	Fixes #7780 (missing lift in expanding alias under a binder in unification).	Hugo Herbelin	2018-06-12
\| \|/ / / / / \|/\| \| \| \| \|
\| * \| \| \| \|	Tweak printing boxes for unicode binders	Ralf Jung	2018-06-10
* \| \| \| \| \|	Fixing #7700 (section variables bound to abbreviations were not found).	Hugo Herbelin	2018-06-10
\|/ / / / /
\| \| \| \| *	Existing Class noop when already a class + warning.	Gaëtan Gilbert	2018-06-08
\| \|_\|_\|/ \|/\| \| \|
* \| \| \|	add test for #7595	Ralf Jung	2018-06-07
\| \| \| *	Fix #7615: Functor inlining drops universe substitution.	Pierre-Marie Pédrot	2018-06-07
\| \|_\|/ \|/\| \|
* \| \|	Merge PR #7077: Preserving canonical structure of return predicate in vm_comp...	Maxime Dénès	2018-06-05
\|\ \ \
* \ \ \	Merge PR #7663: test suite: make target to regenerate failing output tests	Enrico Tassi	2018-06-05
\|\ \ \ \
* \| \| \| \|	Fix #7631: native_compute fails to compile an example in Coq 8.8	Maxime Dénès	2018-06-04
* \| \| \| \|	Merge PR #7315: An attempt to clarify error message for Arguments needing "re...	Maxime Dénès	2018-06-04
\|\ \ \ \ \
\| \| \| * \| \|	Tests for part of #7068 and for #7076 (vm/native_compute and return predicate).	Hugo Herbelin	2018-06-04
\| \|_\|/ / / \|/\| \| \| \|
* \| \| \| \|	Merge PR #7229: Deprecate implicit tactic solving.	Hugo Herbelin	2018-06-04
\|\ \ \ \ \
\| \| \| * \| \|	test suite: make target to regenerate failing output tests	Gaëtan Gilbert	2018-06-04
* \| \| \| \| \|	Merge PR #7199: Fixes #7195: missing freshness condition in Ltac pattern-matc...	Matthieu Sozeau	2018-06-04
\|\ \ \ \ \ \
* \ \ \ \ \ \	Merge PR #7112: Fix #6770: fixpoint loses locality info in proof mode.	Matthieu Sozeau	2018-06-04
\|\ \ \ \ \ \ \
* \ \ \ \ \ \ \	Merge PR #7114: Fix #7113: Program Let Fixpoint in section causes anomaly	Matthieu Sozeau	2018-06-04
\|\ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \	Merge PR #7189: Fix #5539: algebraic universe produced by cases.	Matthieu Sozeau	2018-06-04
\|\ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \	Merge PR #7013: Fixes #7011: Fix/CoFix were not considered in main loop of ta...	Matthieu Sozeau	2018-06-04
\|\ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \	Merge PR #7552: Fix #7539: Checker does not properly handle negative coinduct...	Matthieu Sozeau	2018-06-04
\|\ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \	Merge PR #7590: Fix #7586: Anomaly "Uncaught exception Not_found".	Matthieu Sozeau	2018-06-04
\|\ \ \ \ \ \ \ \ \ \ \ \
\| \| \| \| \| \| \| \| * \| \| \| \|	Deprecate implicit tactic solving.	Pierre-Marie Pédrot	2018-06-04
\| \|_\|_\|_\|_\|_\|_\|/ / / / / \|/\| \| \| \| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \| \| \| \|	Merge PR #7496: Fix #4403: insufficient handling of type-in-type in kernel.	Maxime Dénès	2018-06-04
\|\ \ \ \ \ \ \ \ \ \ \ \ \| \|_\|_\|_\|_\|_\|_\|_\|_\|/ / / \|/\| \| \| \| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \| \| \| \|	Merge PR #7578: Allow make clean to work on a fresh clone	Enrico Tassi	2018-05-31
\|\ \ \ \ \ \ \ \ \ \ \ \
\| \| \| \| \| \| \| * \| \| \| \| \|	Fix #7113: Program Let Fixpoint in section causes anomaly	Gaëtan Gilbert	2018-05-30
* \| \| \| \| \| \| \| \| \| \| \| \|	Fix #6951: Unexpected error during scheme creation.	Pierre-Marie Pédrot	2018-05-29
\| \|_\|_\|_\|_\|_\|/ / / / / / \|/\| \| \| \| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \| \| \| \|	Add test for #7333: vm_compute segfaults / Anomaly with cofix	Maxime Dénès	2018-05-29
\| * \| \| \| \| \| \| \| \| \| \|	Allow make clean to work on a fresh clone	Jason Gross	2018-05-25
\| \| \| \| \| \| \| \| \| * \| \|	An attempt to clarify error message for Arguments needing "rename" flag.	Hugo Herbelin	2018-05-25
\| \|_\|_\|_\|_\|_\|_\|_\|/ / / \|/\| \| \| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \| \| \|	Fix #7323: coqchk puts polymorphic univs of inductive in global env	Gaëtan Gilbert	2018-05-24
* \| \| \| \| \| \| \| \| \| \|	Merge PR #7328: Fix #7327: coqchk subtyping of polymorphic constants	Pierre-Marie Pédrot	2018-05-24
\|\ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \	Merge PR #7317: Fix #6798: coqchk ignores ugraph when comparing constant inst...	Pierre-Marie Pédrot	2018-05-24
\|\ \ \ \ \ \ \ \ \ \ \ \
\| \| \| \| \| * \| \| \| \| \| \| \|	Fix #7586: Anomaly "Uncaught exception Not_found".	Pierre-Marie Pédrot	2018-05-23
\| \|_\|_\|_\|/ / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \| \| \| \|	Merge PR #7567: Clean-up dead file in test-suite.	Enrico Tassi	2018-05-23
\|\ \ \ \ \ \ \ \ \ \ \ \ \| \|_\|_\|/ / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \| \| \| \|	Add test cases from #7554	Tej Chajed	2018-05-20
\| \| \| \| \| * \| \| \| \| \| \|	Fix #7539: Checker does not properly handle negative coinductive types.	Pierre-Marie Pédrot	2018-05-18
\| \|_\|_\|_\|/ / / / / / / \|/\| \| \| \| \| \| \| \| \| \|
\| * \| \| \| \| \| \| \| \| \|	Clean-up dead file in test-suite.	Théo Zimmermann	2018-05-18
\|/ / / / / / / / / /
* \| \| \| \| \| \| \| \| \|	Merge PR #7451: Introduce an option to allow nested lemma, and turn it off by...	Emilio Jesus Gallego Arias	2018-05-17
\|\ \ \ \ \ \ \ \ \ \
\| * \| \| \| \| \| \| \| \| \|	Introduce an option to allow nested lemma, and turn it off by default.	Théo Zimmermann	2018-05-17
* \| \| \| \| \| \| \| \| \| \|	Modify make system to include Makefile.common in the test suite	Gaëtan Gilbert	2018-05-16
* \| \| \| \| \| \| \| \| \| \|	unit tests: add .merlin	Gaëtan Gilbert	2018-05-16
* \| \| \| \| \| \| \| \| \| \|	add unit tests to test suite	Paul Steckler	2018-05-16
\|/ / / / / / / / / /
* \| \| \| \| \| \| \| \| \|	Merge PR #7484: Fix non-portable shebang in test-suite.	Enrico Tassi	2018-05-16
\|\ \ \ \ \ \ \ \ \ \
* \| \| \| \| \| \| \| \| \| \|	[ssr] import ssreflect test suite from math-comp	Enrico Tassi	2018-05-15
* \| \| \| \| \| \| \| \| \| \|	Merge PR #7502: Fixing little printing bug with "Locate" on recursive notations	Emilio Jesus Gallego Arias	2018-05-14
\|\ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \	Merge PR #7479: Move 4722 (dangling symlink) to misc tests, remove dangling s...	Gaëtan Gilbert	2018-05-14
\|\ \ \ \ \ \ \ \ \ \ \ \
\| \| * \| \| \| \| \| \| \| \| \| \|	Fixing a bug in printing the body of a located notation.	Hugo Herbelin	2018-05-13
\| \|/ / / / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \|
\| * \| \| \| \| \| \| \| \| \| \|	Move 4722 (dangling symlink) to misc tests, remove dangling symlink from repo	Ralf Jung	2018-05-13
* \| \| \| \| \| \| \| \| \| \| \|	Merge PR #7477: Support for notations with autonomous only-parsing and only-p...	Emilio Jesus Gallego Arias	2018-05-13
\|\ \ \ \ \ \ \ \ \ \ \ \
\| \| \| \| \| \| * \| \| \| \| \| \|	Fix #4403: insufficient handling of type-in-type in kernel.	Gaëtan Gilbert	2018-05-13
\| \|_\|_\|_\|_\|/ / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \| \| \| \|	Merge PR #7470: use at least 6 Xs in mktemp filename templates	Gaëtan Gilbert	2018-05-11
\|\ \ \ \ \ \ \ \ \ \ \ \