coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Typeclass backtracking example by J. Leivant	Matthieu Sozeau	2016-09-28
\|
*	Merge remote-tracking branch 'github/pr/232' into v8.6	Maxime Dénès	2016-09-28
\|\ \| \| \| \| \| \|	Was PR#232: Fix the parsing of goal selectors.
* \|	Add fixed test-suite file for bug #4527	Matthieu Sozeau	2016-09-27
\| \|
* \|	Unbreak Ltac [ \| .. \| ] notation in -compat 8.5	Jason Gross	2016-09-26
\| \| \| \| \| \| \| \| \| \| \| \|	Importing VectorNotations breaks `; []`. So we make sure it's not imported by defualt. Some files might be required to `Import VectorDef.VectorNotations` rather than just `Import VectorNotations`.
* \|	Fix bug #4785 (use [ ] for vector nil)	Jason Gross	2016-09-26
\| \| \| \| \| \| \| \| \| \|	Also delimit vector_scope with vector, so that people can write %vector without having to delimit it themselves.
* \|	Posssible abstractions over goal variables when inferring match return clause.	Hugo Herbelin	2016-09-26
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	The no-inversion and maximal abstraction over dependencies now supports abstraction over goal variables rather than only on "rel" variables. In particular, it now works consistently using "intro H; refine (match H with ... end)" or "refine (fun H => match H with ... end)". By doing so, we ensure that all three strategies are tried in all situations where a return clause has to be inferred, even in the context of a "refine". See antepenultimate commit for discussion.
* \|	Trying an abstracting dependencies heuristic for the match return clause ↵	Hugo Herbelin	2016-09-26
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	even when no type constraint is given. This no-inversion and maximal abstraction over dependencies in (rel) variables heuristic was used only when a type constraint was given. By doing so, we ensure that all three strategies "inversion with dependencies as evars", "no-inversion and maximal abstraction over dependencies in (rel) variables", "no-inversion and no abstraction over dependencies" are tried in all situations where a return clause has to be inferred. See penultimate commit for discussion.
* \|	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
\|\\| \| \|