diff options
| -rw-r--r-- | test-suite/bugs/closed/3628.v (renamed from test-suite/bugs/opened/3628.v) | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/test-suite/bugs/opened/3628.v b/test-suite/bugs/closed/3628.v index bd85bb1f92..4001cf7c2b 100644 --- a/test-suite/bugs/opened/3628.v +++ b/test-suite/bugs/closed/3628.v @@ -5,5 +5,5 @@ End NonPrim. Module Prim. Set Primitive Projections. Class AClass := { x : Set }. - Fail Arguments x {AClass}. + Arguments x {AClass}. End Prim. |