diff options
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/bugs/closed/3289.v (renamed from test-suite/bugs/opened/3289.v) | 8 |
1 files changed, 7 insertions, 1 deletions
diff --git a/test-suite/bugs/opened/3289.v b/test-suite/bugs/closed/3289.v index 63453c5b81..4542b015d0 100644 --- a/test-suite/bugs/opened/3289.v +++ b/test-suite/bugs/closed/3289.v @@ -11,7 +11,13 @@ Instance contr_unit : Contr Unit | 0 := contr := fun t : Unit => I |} in x. (* success *) -Fail Instance contr_unit' : Contr Unit | 0 := +Instance contr_internal_unit' : Contr_internal Unit | 0 := + {| + center := tt; + contr := fun t : Unit => I + |}. + +Instance contr_unit' : Contr Unit | 0 := {| center := tt; contr := fun t : Unit => I |