diff options
| -rw-r--r-- | test-suite/bugs/closed/4301.v | 9 |
1 files changed, 1 insertions, 8 deletions
diff --git a/test-suite/bugs/closed/4301.v b/test-suite/bugs/closed/4301.v index 1a8d3611bf..3b00efb213 100644 --- a/test-suite/bugs/closed/4301.v +++ b/test-suite/bugs/closed/4301.v @@ -4,14 +4,7 @@ Module Type Foo. Parameter U : Type. End Foo. -(* Module Lower (X : Foo). *) -(* Definition U' : Prop := X.U@{Prop}. *) -(* End Lower. *) -(* Module Lower (X : Foo with Definition U := Prop). *) -(* Definition U' := X.U@{Prop}. *) -(* End Lower. *) -Module Lower (X : Foo with Definition U := True). - (* Definition U' : Prop := X.U. *) +Module Lower (X : Foo with Definition U := True : Type). End Lower. Module M : Foo. |