From f4db3d72abc1872839bcacd3b28a439e69d0a2e8 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Thu, 1 Oct 2015 16:41:23 +0200
Subject: Univs: fix test-suite file (4301 is invalid, but a good regression
 test)

---
 test-suite/bugs/closed/4301.v | 9 +--------
 1 file changed, 1 insertion(+), 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.
-- 
cgit v1.2.3