diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2015-10-01 16:41:23 +0200 |
|---|---|---|
| committer |  Matthieu Sozeau <mattam@mattam.org> | 2015-10-02 15:54:13 +0200 |
| commit | f4db3d72abc1872839bcacd3b28a439e69d0a2e8 (patch) | |
| tree | aa5dbdcca255e36e01ed3470a0808a4514d9f7e2 /test-suite/bugs/closed/4301.v | |
| parent | b144ef5e2698932c5b2f7cdb1688a55ce4764dae (diff) | |
Univs: fix test-suite file (4301 is invalid, but a good regression test)
Diffstat (limited to 'test-suite/bugs/closed/4301.v')
| -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 1a8d3611b..3b00efb21 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. |