coq - the Coq proof assistant

	Commit message (Collapse)	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
\|/ / / / / \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Redundancy between finding section variables in both interp_var and interp_qualid could probably be cleaned.
\| \| \| \| *	Existing Class noop when already a class + warning.	Gaëtan Gilbert	2018-06-08
\| \|_\|_\|/ \|/\| \| \| \| \| \| \| \| \| \| \|	Fix #5012.
* \| \| \|	add test for #7595	Ralf Jung	2018-06-07
\| \| \| \|
\| \| \| *	Fix #7615: Functor inlining drops universe substitution.	Pierre-Marie Pédrot	2018-06-07
\| \|_\|/ \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	We store the universe context in the inlined terms and apply it to the instance provided to the substitution function. Technically the context is not needed, but we use it to assert that the length of the instance corresponds, just in case.
* \| \|	Merge PR #7077: Preserving canonical structure of return predicate in ↵	Maxime Dénès	2018-06-05
\|\ \ \ \| \| \| \| \| \| \| \| \| \| \| \|	vm_compute and native_compute (partial fix to #7068; also fixes #7076))
* \ \ \	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
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Dependency analysis for separate compilation was not iterated properly on rel_context and named_context.
* \| \| \| \|	Merge PR #7315: An attempt to clarify error message for Arguments needing ↵	Maxime Dénès	2018-06-04
\|\ \ \ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	"rename" flag
\| \| \| * \| \|	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 ↵	Matthieu Sozeau	2018-06-04
\|\ \ \ \ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	pattern-matching names
* \ \ \ \ \ \	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 ↵	Matthieu Sozeau	2018-06-04
\|\ \ \ \ \ \ \ \ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	tactic unification.
* \ \ \ \ \ \ \ \ \ \	Merge PR #7552: Fix #7539: Checker does not properly handle negative ↵	Matthieu Sozeau	2018-06-04
\|\ \ \ \ \ \ \ \ \ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	coinductive types.
* \ \ \ \ \ \ \ \ \ \ \	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
\| \|_\|_\|_\|_\|_\|/ / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	When creating a scheme for bifinite inductive types, we do not create a fixpoint.
* \| \| \| \| \| \| \| \| \| \| \|	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
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	The file `config/Makefile` doesn't exist unless we run `./configure`. We shouldn't have to run `./configure` to run `make clean`. We now no longer error in any case if `config/Makefile` doesn't exist; this is simpler than only not erroring if the target is `clean`. We also now test this property when building on CI. This fixes #7542
\| \| \| \| \| \| \| \| \| * \| \|	An attempt to clarify error message for Arguments needing "rename" flag.	Hugo Herbelin	2018-05-25
\| \|_\|_\|_\|_\|_\|_\|_\|/ / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Using a formulation which makes it is clear that no renaming has been done. See discussion at issue #2987.
* \| \| \| \| \| \| \| \| \| \|	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 ↵	Pierre-Marie Pédrot	2018-05-24
\|\ \ \ \ \ \ \ \ \ \ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	instances
\| \| \| \| \| * \| \| \| \| \| \| \|	Fix #7586: Anomaly "Uncaught exception Not_found".	Pierre-Marie Pédrot	2018-05-23
\| \|_\|_\|_\|/ / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	The old unification engine was using the unfiltered environment when a context had been cleared, leading to an ill-typed goal.
* \| \| \| \| \| \| \| \| \| \| \|	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
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Failed in v8.7.2 but were fixed by v8.8.0.
\| \| \| \| \| * \| \| \| \| \| \|	Fix #7539: Checker does not properly handle negative coinductive types.	Pierre-Marie Pédrot	2018-05-18
\| \|_\|_\|_\|/ / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	The reduction machine of the checker was not taking into account the fact that cofixpoints needed to be unfolded when applied against a projection.
\| * \| \| \| \| \| \| \| \| \|	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 ↵	Emilio Jesus Gallego Arias	2018-05-17
\|\ \ \ \ \ \ \ \ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	by default.
\| * \| \| \| \| \| \| \| \| \|	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 ↵	Gaëtan Gilbert	2018-05-14
\|\ \ \ \ \ \ \ \ \ \ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	symlink from repo
\| \| * \| \| \| \| \| \| \| \| \| \|	Fixing a bug in printing the body of a located notation.	Hugo Herbelin	2018-05-13
\| \|/ / / / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	This was introduced between v8.5 and v8.6 (presumably 63f3ca8).
\| * \| \| \| \| \| \| \| \| \| \|	Move 4722 (dangling symlink) to misc tests, remove dangling symlink from repo	Ralf Jung	2018-05-13
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Fixes #7065
* \| \| \| \| \| \| \| \| \| \| \|	Merge PR #7477: Support for notations with autonomous only-parsing and ↵	Emilio Jesus Gallego Arias	2018-05-13
\|\ \ \ \ \ \ \ \ \ \ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	only-printing declarations.
\| \| \| \| \| \| * \| \| \| \| \| \|	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
\|\ \ \ \ \ \ \ \ \ \ \ \