diff --git a/src/kernel_internals/typing/rmtmps.ml b/src/kernel_internals/typing/rmtmps.ml index 496842818065bbd43ca7fbb95954bb1f0cf4ffe6..4a6a6f796373b8d2bcd6893dd2d91e0b52969cfe 100644 --- a/src/kernel_internals/typing/rmtmps.ml +++ b/src/kernel_internals/typing/rmtmps.ml @@ -881,9 +881,6 @@ let removeUnmarked isRoot ast reachable_tbl = * *) - -type rootsFilter = global -> bool - let removeUnused ?(isRoot=isExportedRoot) ast = if not !keepUnused then begin