From 9ac005d89776bf74e78875128f04620c40a9408b Mon Sep 17 00:00:00 2001
From: barras
Date: Tue, 22 Apr 2008 11:11:46 +0000
Subject: fixed universes bug related to module inclusion

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10828 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 test-suite/failure/univ_include.v | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

(limited to 'test-suite')

diff --git a/test-suite/failure/univ_include.v b/test-suite/failure/univ_include.v
index fd17457f09..4be70d888c 100644
--- a/test-suite/failure/univ_include.v
+++ b/test-suite/failure/univ_include.v
@@ -17,13 +17,14 @@ Module G (E : MU).
   Include F E.
 Print Universes. (* U <= T *)
 End G.
-Print Universes. (* constraint lost! *)
+Print Universes. (* Check if constraint is lost *)
 
 Module Mt.
-  Definition t :=T.
+  Definition t := T.
 End Mt.
 
-Module P := G Mt.
+Module P := G Mt. (* should yield Universe inconsistency *)
+(* ... otherwise the following command will show that T has type T! *)
 Eval cbv delta [P.elt Mt.t] in P.elt.
 
 
-- 
cgit v1.2.3