diff options
| author | Matthieu Sozeau | 2014-06-11 16:55:29 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2014-06-11 16:55:29 +0200 |
| commit | 99cdbc25a3a92545544a087ed55240c488b42fc9 (patch) | |
| tree | 4b9f80d7ae15a421b5745dec138759a37cf68da6 /test-suite | |
| parent | 1c620d266885086e076011917d5b1d28af299ea1 (diff) | |
Fix bug #3289
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 |