diff --git a/src/kernel_internals/typing/ghost_cfg.mli b/src/kernel_internals/typing/ghost_cfg.mli index fa8f3783c350c4298ad978d4b3764d4dada56ad8..3a4c651b14c3abc304c0ae058e063a1e3d80e5f4 100644 --- a/src/kernel_internals/typing/ghost_cfg.mli +++ b/src/kernel_internals/typing/ghost_cfg.mli @@ -19,3 +19,9 @@ (* for more details (enclosed in the file licenses/LGPLv2.1). *) (* *) (**************************************************************************) + +(** Checks that normal cfg is not altered by ghost statements. + Registered as a transformation category (that doesn't transform + anything but will complain if ghost cfg is ill-formed) +*) +val transform_category: File.code_transformation_category