Close #11133

Fixed by 8750682e367d7e78634bf88e667e4c9e7c3613d3 (#9915)

1 files changed, 18 insertions, 0 deletions

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.