diff options
| author | Hugo Herbelin | 2014-12-03 13:15:03 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2014-12-03 19:26:16 +0100 |
| commit | dfeaea43d9e692984cf430f4f19ec527625586ea (patch) | |
| tree | 7c90f655e8ffc41523c12ea1a0fb6ca87f8faf21 | |
| parent | 3b85b2bb48261ed262106e5591fa459bd3d94d73 (diff) | |
Updading test-suite.
| -rw-r--r-- | test-suite/bugs/closed/3682.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/test-suite/bugs/closed/3682.v b/test-suite/bugs/closed/3682.v index 71baf78cf2..b8c5b4d524 100644 --- a/test-suite/bugs/closed/3682.v +++ b/test-suite/bugs/closed/3682.v @@ -2,4 +2,4 @@ Class Foo. Definition bar `{Foo} (x : Set) := Set. Instance: Foo. Definition bar1 := bar nat. -Fail Definition bar2 := bar $(admit)$. +Definition bar2 := bar $(admit)$. |