diff options
Diffstat (limited to 'kernel/names.ml')
| -rw-r--r-- | kernel/names.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/kernel/names.ml b/kernel/names.ml index fbd26ca3d..0da8fc5d4 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -234,6 +234,7 @@ struct end module MBImap = Map.Make(MBId) +module MBIset = Set.Make(MBId) (** {6 Names of structure elements } *) |