test module include w.r.t. universe constraints

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10827 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 29 insertions, 0 deletions

diff --git a/test-suite/failure/univ_include.v b/test-suite/failure/univ_include.v
new file mode 100644
index 000000000..fd17457f0
--- /dev/null
+++ b/test-suite/failure/univ_include.v
@@ -0,0 +1,29 @@
+Definition T := Type.
+Definition U := Type.
+
+Module Type MT. 
+  Parameter t : T.
+End MT. 
+
+Module Type MU.
+  Parameter t : U.
+End MU.
+
+Module F (E : MT).
+  Definition elt :T := E.t.
+End F.
+
+Module G (E : MU).
+  Include F E.
+Print Universes. (* U <= T *)
+End G.
+Print Universes. (* constraint lost! *)
+
+Module Mt.
+  Definition t :=T.
+End Mt.
+
+Module P := G Mt.
+Eval cbv delta [P.elt Mt.t] in P.elt.
+
+