aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/bugs/closed
diff options
context:
space:
mode:
authorGravatar Matthieu Sozeau <matthieu.sozeau@inria.fr>2015-10-01 16:41:23 +0200
committerGravatar Matthieu Sozeau <mattam@mattam.org>2015-10-02 15:54:13 +0200
commitf4db3d72abc1872839bcacd3b28a439e69d0a2e8 (patch)
treeaa5dbdcca255e36e01ed3470a0808a4514d9f7e2 /test-suite/bugs/closed
parentb144ef5e2698932c5b2f7cdb1688a55ce4764dae (diff)
Univs: fix test-suite file (4301 is invalid, but a good regression test)
Diffstat (limited to 'test-suite/bugs/closed')
-rw-r--r--test-suite/bugs/closed/4301.v9
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.