Module Mcfg

module Mcfg: sig .. end

This is what is really needed to propagate something through the CFG. Usually, the propagated thing should be a predicate, but it can be more sophisticated like lists of predicates, or maybe a structure to keep hypotheses and goals separated. Moreover, proof obligations may also need to be handeled.

type scope = 

module type Export = sig .. end

module type Splitter = sig .. end

module type S = sig .. end