Documentation

Run before serialisation to remove data that's not reachable from the public interface. We do not compute reachable data precisely, because that would be very expensive, mainly because of rewrite rules. The following things are assumed to be "roots": - public definitions - definitions marked as primitive - definitions with COMPILE pragma - all pattern synonyms (because currently all of them go into interfaces) - all parameter sections (because currently all of them go into interfaces) (see also issues #6931 and #7382) - local builtins - all rewrite rules - closed display forms We only ever prune dead metavariables and definitions. We return the pruned metas, pruned definitions and closed display forms.