Monads.CmpM
The "computation" monad; contains enough state to run computations in the semantic domain, does not contain a variable environment or anything that would be needed for evaluation.
val read_global : RefineState.t m
val restore_cof_thy : CodeUnit.CofThy.Disj.t -> 'a m -> 'a m