coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
* \| \| \| \| \| \| \| \| \| \| \|	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
\|\ \ \ \ \ \ \ \ \ \ \ \
\| \| \| \| * \| \| \| \| \| \| \| \|	Fix non-portable shebang in test-suite.	Théo Zimmermann	2018-05-11
\| \|_\|_\|/ / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \| \| \| \|	Merge PR #7363: [ci] Fix another issue with the timing tests	Gaëtan Gilbert	2018-05-11
\|\ \ \ \ \ \ \ \ \ \ \ \
\| \| \| * \| \| \| \| \| \| \| \| \|	Fixes #7462, part 2 (only-printing not make believe parsing rule is declared).	Hugo Herbelin	2018-05-10
\| \| \| * \| \| \| \| \| \| \| \| \|	Fixes part 1 of #7462 (only-printing not to override existing interp rule).	Hugo Herbelin	2018-05-10
\| \| \| \|/ / / / / / / / /
\| \| * / / / / / / / / /	use at least 6 Xs in mktemp filename templates	Sven M. Hallberg	2018-05-09
\| \| \|/ / / / / / / / /
* \| / / / / / / / / /	test for coqc -o	Enrico Tassi	2018-05-09
\| \|/ / / / / / / / / \|/\| \| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \| \|	Merge PR #7134: When an error comes from loading the prelude, tell it happene...	Emilio Jesus Gallego Arias	2018-05-03
\|\ \ \ \ \ \ \ \ \ \
\| * \| \| \| \| \| \| \| \| \|	Making explicit that errors happen in one of five executation phases.	Hugo Herbelin	2018-05-02
* \| \| \| \| \| \| \| \| \| \|	Make "intro"/"intros" progress on existential variables.	Hugo Herbelin	2018-05-02
\|/ / / / / / / / / /
* \| \| \| \| \| \| \| \| \|	Strict focusing using Default Goal Selector.	Gaëtan Gilbert	2018-04-29
\| * \| \| \| \| \| \| \| \|	[ci] Fix another issue with the timing tests	Jason Gross	2018-04-26
* \| \| \| \| \| \| \| \| \|	Pretyping: Fixing a de Bruijn bug in interpreting default instances of evars.	Hugo Herbelin	2018-04-26
\|/ / / / / / / / /
\| \| * / / / / / /	Fix #7327: coqchk subtyping of polymorphic constants	Gaëtan Gilbert	2018-04-23
\| \|/ / / / / / /
* \| \| \| \| \| \| \|	test suite: clean more things (glob, MExtraction.out, distclean aux)	Gaëtan Gilbert	2018-04-22
* \| \| \| \| \| \| \|	test suite: print message for failing tests as they come	Gaëtan Gilbert	2018-04-22
* \| \| \| \| \| \| \|	test suite Makefile: do not use %.stamp for subsystem targets	Gaëtan Gilbert	2018-04-22
\| * \| \| \| \| \| \|	Fix #6798: coqchk ignores ugraph when comparing constant instances	Gaëtan Gilbert	2018-04-20
\|/ / / / / / /
* \| \| \| \| \| \|	Merge PR #7237: [ssr] fix delayed clears (fix #7045)	Maxime Dénès	2018-04-16
\|\ \ \ \ \ \ \
* \| \| \| \| \| \| \|	[ltac] Deprecate nameless fix/cofix.	Emilio Jesus Gallego Arias	2018-04-13
\| * \| \| \| \| \| \|	[ssr] fix delayed clears (fix #7045)	Enrico Tassi	2018-04-13
\|/ / / / / / /
* \| \| \| \| \| \|	Merge PR #7179: Fix #5981, bugs/opened/3263.v is non-deterministic by removin...	Jason Gross	2018-04-12
\|\ \ \ \ \ \ \
* \ \ \ \ \ \ \	Merge PR #500: Move bugs that have been closed on Bugzilla	Maxime Dénès	2018-04-12
\|\ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \	Merge PR #7087: Congruence tactic engine update	Pierre-Marie Pédrot	2018-04-12
\|\ \ \ \ \ \ \ \ \
\| \| * \| \| \| \| \| \| \|	Fix the status of some resolved bugs	Tej Chajed	2018-04-11
\| \|/ / / / / / / / \|/\| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \|	Merge PR #7116: Fixes #7110: missing test on the absence of a "as" while look...	Emilio Jesus Gallego Arias	2018-04-09
\|\ \ \ \ \ \ \ \ \