coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Trying a no-inversion no-dependency heuristic for match return clause.	Hugo Herbelin	2016-09-26
\| \| \| \| \| \| \| \|	The no-inversion no-dependency heuristic was used only in the absence of type constraint. We may now use it also in the presence of a type constraint. See previous commit for discussion.
*	Fix bug #5093: typeclasses eauto depth arg does not accept a var.	Pierre-Marie Pédrot	2016-09-26
\|
*	Adding a test for bug #5096.	Pierre-Marie Pédrot	2016-09-24
\|
*	Merge branch 'v8.5' into v8.6	Pierre-Marie Pédrot	2016-09-23
\|\
\| *	Fixing #5095 (non relevant too strict test in let-in abstraction).	Hugo Herbelin	2016-09-22
\| \|
* \|	Further "decide equality" tests on demand of Jason.	Hugo Herbelin	2016-09-17
\| \|
* \|	Added a test file for contradiction.	Hugo Herbelin	2016-09-15
\| \|
* \|	Continuing fix to #5078, taking also into account intropatterns.	Hugo Herbelin	2016-09-15
\| \| \| \| \| \| \| \|	Getting closer from before when the bug was introduced + test.
* \|	Merge branch 'v8.5' into v8.6	Pierre-Marie Pédrot	2016-09-14
\|\\|
\| *	Fixing test-suite after commit 43104a0b.	Pierre-Marie Pédrot	2016-09-14
\| \|
* \|	test-suite/output-modulo-time made more robust	Enrico Tassi	2016-09-13
\| \|
\| *	Fixing a recursive notation bug raised on coq-club on Sep 12, 2016.	Hugo Herbelin	2016-09-12
\| \|
* \|	Merge remote-tracking branch 'github-coq/pr/249' into v8.6	Matthieu Sozeau	2016-09-12
\|\ \
* \| \|	Add support for testing output mod timing changes	Jason Gross	2016-09-11
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Uses sed 's/\s[0-9]\.[0-9]\+\s//g' and 's/\s0\.\s*//g' to strip numbers of seconds and to strip percentages. (This can potentially be extended later.) Add a test-suite file to make sure that LtacProf outputs some table.
* \| \|	Add a test for 4836	Jason Gross	2016-09-11
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	This required improving the machinery of the test-suite Makefile to support -compile.
\| \| *	Test for #5077.	Hugo Herbelin	2016-09-10
\| \| \|
\| * \|	no-refold patch	Paul Steckler	2016-09-09
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Add a boolean for refolding during reduction, and an option that is off by default in 8.6, to turn refolding on in all reduction functions, as in 8.5.
* \| \|	Fix output test-suite after commit 0d3c319.	Pierre-Marie Pédrot	2016-09-09
\|/ /
* \|	Update csdp cache.	Pierre-Marie Pédrot	2016-09-09
\| \| \| \| \| \| \| \|	This was making the test-suite fail on machines where csdp was not installed.
* \|	Fix Bug #5073 : regression of micromega plugin	Frédéric Besson	2016-09-08
\| \| \| \| \| \| \| \|	esprit d'escalier : is now also fixed for R
* \|	Fix Bug #5073 : regression of micromega plugin	Frédéric Besson	2016-09-08
\| \| \| \| \| \| \| \| \| \|	The computed proof term is now more explicit exact (__arith P1 ... Pn X1 ... Xm) instead of apply (__arith P1 ... Pn) which unification could fail.
* \|	Merge branch 'v8.5' into v8.6	Pierre-Marie Pédrot	2016-09-07
\|\\|
* \|	micromega : more robust generation of proof terms	Frédéric Besson	2016-09-07
\| \| \| \| \| \| \| \| \| \| \| \| \| \|	- Assert a purely arihtmetic sub-goal that is proved independently by reflexion. (This reduces the stress on the conversion test) - Does not use 'abstract' anymore (more natural proof-term) - Fix a parsing bug (certain terms in Prop where not recognized)
\| *	Test file for #5065 - Anomaly: Not a proof by induction	Maxime Dénès	2016-09-05
\| \|
* \|	Merge branch 'v8.5' into v8.6	Pierre-Marie Pédrot	2016-09-02
\|\\|
\| *	Fix test-suite after Frédéric's 6231f07b2.	Maxime Dénès	2016-09-01
\| \|
* \|	Fix Bug #5005 : micromega tactics is now robust to failure of 'abstract'.	Frédéric Besson	2016-08-31
\| \| \| \| \| \| \| \|	If 'abstract' fails e.g. if there are existentials. The tactic runs an abstract-free alternative.
\| *	Fix bug #5043: [Admitted] lemmas pick up section variables.	Pierre-Marie Pédrot	2016-08-31
\| \| \| \| \| \| \| \| \| \| \| \|	We add a flag Keep Admitted Variables that allows to recover the legacy v8.4 behaviour of admitted lemmas. The statement of such lemmas did not depend on the current context variables.
* \|	Fixing output test-suite after warning for inner Requires.	Pierre-Marie Pédrot	2016-08-30
\| \|
* \|	Fix bug #4893: not_evar: unexpected failure in 8.5pl1.	Pierre-Marie Pédrot	2016-08-30
\| \|
* \|	plugin micromega : nra also handles non-linear rational arithmetic over Q ↵	Frédéric Besson	2016-08-30
\| \| \| \| \| \| \| \| \| \| \| \| \| \|	(Fixed #4985) Lqa.v defines the tactics lra and nra working over Q. Lra.v defines the tactics lra and nra working over R.
* \|	Fix bug #3920: eapply masks an hypothesis name.	Pierre-Marie Pédrot	2016-08-30
\| \| \| \| \| \| \| \| \| \| \| \|	The problem came from the fact that the legacy beta-reduction occurring after a rewrite was wrongly applied to the side-conditions of the rewriting step. We restrict it to the correct goal in this patch.
* \|	Fix bug #4764: Syntactic notation externalization breaks.	Pierre-Marie Pédrot	2016-08-28
\| \|
* \|	Fix bug #4904: [Import] does not load intermediately unqualified names of ↵	Pierre-Marie Pédrot	2016-08-23
\| \| \| \| \| \| \| \|	aliases.
* \|	Merge branch 'v8.5' into v8.6	Pierre-Marie Pédrot	2016-08-21
\|\\|
\| *	Fixing an anomaly in printing a unification error message.	Hugo Herbelin	2016-08-20
\| \|
* \|	Test file for bug #4187.	Pierre-Marie Pédrot	2016-08-19
\| \|
* \|	Merge remote-tracking branch 'origin/pr/246' into v8.6	Matthieu Sozeau	2016-08-19
\|\ \
* \| \|	Adding a test for bug #4653.	Pierre-Marie Pédrot	2016-08-18
\| \| \|
* \| \|	Fixing #3070 ("subst" taking properly into account chains of dependencies).	Hugo Herbelin	2016-08-17
\| \| \|
* \| \|	Merge branch 'v8.5' into v8.6	Pierre-Marie Pédrot	2016-08-16
\|\ \ \ \| \| \|/ \| \|/\|
\| * \|	Fix bug #4673: regression in setoid_rewrite.	Matthieu Sozeau	2016-07-29
\| \| \| \| \| \| \| \| \| \| \| \|	Modulo delta for types should be fully transparent.
* \| \|	Merge remote-tracking branch 'gforge/v8.5' into v8.6	Matthieu Sozeau	2016-07-29
\|\\| \|
\| * \|	Fix bug #3886, generation of obligations of fixes	Matthieu Sozeau	2016-07-29
\| \| \| \| \| \| \| \| \| \| \| \|	This partially reverts c14ccd1b8a3855d4eb369be311d4b36a355e46c1
\| * \|	Fix #4769, univ poly and elim schemes in sections	Matthieu Sozeau	2016-07-29
\| \| \|
\| * \|	Fix bug #4754, allow conversion problems to remain	Matthieu Sozeau	2016-07-26
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	when checking that the rewrite relation is homogeneous in setoid_rewrite.
* \| \|	Fix bug #4679, weakened setoid_rewrite unification	Matthieu Sozeau	2016-07-21
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	It should use evar instantiations eagerly during unification of the lhs of the lemma, as in 8.4.
\| * \|	Fix bug #4780: universe leak in letin_tac	Matthieu Sozeau	2016-07-20
\| \| \|
* \| \|	Fix bug #4780: universe leak in letin_tac	Matthieu Sozeau	2016-07-20
\| \| \|
\| * \|	Fix Errors.out missing a dot...	Matthieu Sozeau	2016-07-19
\| \| \|