blob: 87f15a4a19614c7e2fe2f53992b51fe9149841a9 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
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.
|
