coq/test-suite/bugs/closed/shouldsucceed, branch master

Get rid of "shouldsucceed" subdirectory by moving tests to parent directory.

2013-09-20T12:40:28+00:00

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16797 85f007b7-540e-0410-9357-904b9bb8a0f7

Added a test for bug #3062.

2013-08-04T19:01:01+00:00

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16661 85f007b7-540e-0410-9357-904b9bb8a0f7

Added a test for bug #3088.

2013-08-01T17:40:05+00:00

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16650 85f007b7-540e-0410-9357-904b9bb8a0f7

Tentative fix for #3054: we refresh universes in a term generated

2013-07-29T16:35:50+00:00

by congruence, as it seems to be done methodically on the remaining
of this plugin.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16642 85f007b7-540e-0410-9357-904b9bb8a0f7

Fixing bug #3093 by adding the asked test case.

2013-07-25T12:38:46+00:00

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16634 85f007b7-540e-0410-9357-904b9bb8a0f7

Bugfix: Fixing #3050

2013-06-27T14:31:03+00:00

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16608 85f007b7-540e-0410-9357-904b9bb8a0f7

Added a unit test for bug #2230.

2013-04-27T23:21:42+00:00

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16460 85f007b7-540e-0410-9357-904b9bb8a0f7

Finer fix for bug 3017, mark unresolvability only of goals that are

2013-04-18T15:26:08+00:00

instances of metas in clenvtac. Makes Math-Classes compile again.


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16429 85f007b7-540e-0410-9357-904b9bb8a0f7

Equality: avoid some unprotected List.nth (fix #2837)

2013-04-10T09:03:08+00:00

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16392 85f007b7-540e-0410-9357-904b9bb8a0f7

Enrich test-suite with a test for #3022.

2013-04-08T13:16:46+00:00

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16390 85f007b7-540e-0410-9357-904b9bb8a0f7