coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Merge PR #7578: Allow make clean to work on a fresh clone	Enrico Tassi	2018-05-31
\|\
* \|	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
* \|	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
* \ \ \	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.
\| * \| \|	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.
* \ \ \ \ \	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
\| \| \|/ / / \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	OpenBSD mktemp fails with an error otherwise.
* \| / / /	test for coqc -o	Enrico Tassi	2018-05-09
\| \|/ / / \|/\| \| \|
* \| \| \|	Merge PR #7134: When an error comes from loading the prelude, tell it ↵	Emilio Jesus Gallego Arias	2018-05-03
\|\ \ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	happened at initialization time
\| * \| \| \|	Making explicit that errors happen in one of five executation phases.	Hugo Herbelin	2018-05-02
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	The five phases are command line interpretation, initialization, prelude loading, rcfile loading, and sentence interpretation (only the two latters are located). We then parameterize the feedback handler with the given execution phase, so as to possibly annotate the message with information pertaining to the phase.
* \| \| \| \|	Make "intro"/"intros" progress on existential variables.	Hugo Herbelin	2018-05-02
\|/ / / /
* \| \| \|	Strict focusing using Default Goal Selector.	Gaëtan Gilbert	2018-04-29
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	We add a [SelectAlreadyFocused] constructor to [goal_selector] (read "!") which causes a failure when there's not exactly 1 goal and otherwise is a noop. Then [Set Default Goal Selector "!".] puts us in "strict focusing" mode where we can only run tactics if we have only one goal or use a selector. Closes #6689.
\| * \| \|	[ci] Fix another issue with the timing tests	Jason Gross	2018-04-26
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	There was recently a spurious failure on AppVeyor (I've forgotten which PR). This commit fixes that particular failure.
* \| \| \|	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
\| \| \| \| \| \| \| \|	NB: I made .aux be cleaned only with distclean imitating the main Makefile.
* \|	test suite: print message for failing tests as they come	Gaëtan Gilbert	2018-04-22
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	ie you might see make TEST bugs/closed/1337.v TEST bugs/closed/3263.v TEST bugs/closed/7777.v FAILED bugs/closed/3263.v.log TEST bugs/opened/1.v ... report: 3263 failed (should be closed)
* \|	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
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	LTAC's `fix` and `cofix` do require access to the proof object inside the tactic monad when used without a name. This is a bit inconvenient as we aim to make the handling of the proof object purely functional. Alternatives have been discussed in #7196, and it seems that deprecating the nameless forms may have the best cost/benefit ratio, so opening this PR for discussion. See also #6171.
\| *	[ssr] fix delayed clears (fix #7045)	Enrico Tassi	2018-04-13
\|/ \| \| \| \|	We take into account all future ipats, not just the ones in the current branch
*	Merge PR #7179: Fix #5981, bugs/opened/3263.v is non-deterministic by ↵	Jason Gross	2018-04-12
\|\ \| \| \| \| \| \|	removing the test.
* \	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 ↵	Emilio Jesus Gallego Arias	2018-04-09
\|\ \ \ \| \| \| \| \| \| \| \| \| \| \| \|	looking for a notation for a nested pattern
* \ \ \	Merge PR #7176: Fix #6956: Uncaught exception in bytecode compilation	Pierre-Marie Pédrot	2018-04-09
\|\ \ \ \
* \ \ \ \	Merge PR #7165: [ssr] check cleared hyps do exist (fix #7050)	Maxime Dénès	2018-04-09
\|\ \ \ \ \