From b58379a9dbe1eaff122092925898ae8d51265da9 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Wed, 8 Jan 2020 15:05:43 +0100
Subject: Close #11133

Fixed by 8750682e367d7e78634bf88e667e4c9e7c3613d3 (#9915)
---
 test-suite/bugs/closed/bug_11133.v | 18 ++++++++++++++++++
 1 file changed, 18 insertions(+)
 create mode 100644 test-suite/bugs/closed/bug_11133.v

diff --git a/test-suite/bugs/closed/bug_11133.v b/test-suite/bugs/closed/bug_11133.v
new file mode 100644
index 0000000000..87f15a4a19
--- /dev/null
+++ b/test-suite/bugs/closed/bug_11133.v
@@ -0,0 +1,18 @@
+Module Type Universe.
+Parameter U : nat.
+End Universe.
+
+Module Univ_prop (Univ : Universe).
+Include Univ.
+End Univ_prop.
+
+Module Monad (Univ : Universe).
+Module UP := (Univ_prop Univ).
+End Monad.
+
+Module Rules (Univ:Universe).
+Module MP := Monad Univ.
+Include MP.
+Import UP.
+Definition M := UP.U.    (* anomaly here *)
+End Rules.
-- 
cgit v1.2.3