summaryrefslogtreecommitdiff
path: root/test-suite/failure/circular_subtyping1.v
blob: 0b3a8688e084f6160a8c8eeea02a8b415dcaa6fd (plain)
1
2
3
4
5
6
7
(* subtyping verification in presence of  pseudo-circularity*)
Module Type S. End S.
Module Type T. Declare Module M:S. End T.

Module N:S. End N.
Module NN <: T. Module M:=N. End NN.
Module P <: T with Module M:=NN := NN.