diff options
Diffstat (limited to 'plugins/extraction/miniml.mli')
| -rw-r--r-- | plugins/extraction/miniml.mli | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/plugins/extraction/miniml.mli b/plugins/extraction/miniml.mli index edebba49d..5e967ef37 100644 --- a/plugins/extraction/miniml.mli +++ b/plugins/extraction/miniml.mli @@ -187,8 +187,6 @@ type ml_structure = (ModPath.t * ml_module_structure) list type ml_signature = (ModPath.t * ml_module_sig) list -type ml_flat_structure = ml_structure_elem list - type unsafe_needs = { mldummy : bool; tdummy : bool; |