From e94b20b3d61ca9d6694f2ec486f1bdd1f502d675 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 19 Jan 2007 17:16:58 +0000
Subject: Prise en compte des univers algébriques dans les types inférés dans
 les interfaces de module (bug similaire à #1302 mais pour les définitions --
 au lieu des inductifs)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9505 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 test-suite/modules/subtyping.v | 9 +++++++++
 1 file changed, 9 insertions(+)

(limited to 'test-suite/modules')

diff --git a/test-suite/modules/subtyping.v b/test-suite/modules/subtyping.v
index fb3eae3af5..2df8e84e5c 100644
--- a/test-suite/modules/subtyping.v
+++ b/test-suite/modules/subtyping.v
@@ -35,3 +35,12 @@ End TT. (* Generates Top.6 <= Top.1 (+ auxiliary constraints for L_rect) *)
 
 (* Note: Top.6 <= Top.1 is generated by subtyping on A; 
    subtyping of L follows and has not to be checked *)
+
+
+
+(* The same bug as #1302 but for Definition *)
+(* Check that inferred algebraic universes in interfaces are considered *)
+
+Module Type U. Definition A := Type -> Type. End U.
+Module M:U. Definition A := Type -> Type. End M.
+
-- 
cgit v1.2.3