diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-04-07 22:01:23 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-04-07 22:01:23 +0000 |
| commit | fe3db6e9f688af4c9da29f6508c285bf42324eab (patch) | |
| tree | d571da4ebbc514efb209bb0a3420033b1a581503 /test-suite | |
| parent | 7672bf2bdb941fd487e6c4a0e7deff1143bff680 (diff) | |
Granting wish #2251 thanks to commit 12900 solved bug 1416.v (which
was actually failing for another reason than the reason originally
filled in the bug tracker) and revealed a bug in the unification.v
test file.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12906 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/bugs/closed/shouldsucceed/1416.v (renamed from test-suite/bugs/opened/shouldnotfail/1416.v) | 0 |
1 files changed, 0 insertions, 0 deletions
diff --git a/test-suite/bugs/opened/shouldnotfail/1416.v b/test-suite/bugs/closed/shouldsucceed/1416.v index da67d9b04..da67d9b04 100644 --- a/test-suite/bugs/opened/shouldnotfail/1416.v +++ b/test-suite/bugs/closed/shouldsucceed/1416.v |