RelationPriv.DownwardClosedClusterClusters when clustering is downward-closed.
module ClusteringArg : ClusteringArgmodule RD : RelationDomain.RDmodule VS : sig ... endmodule LRD : sig ... endmodule Cluster = VSval keep_only_protected_globals :
Queries.ask ->
LockDomain.MustLock.t ->
LRD.t ->
LRD.t