diff options
Diffstat (limited to 'intf/misctypes.mli')
| -rw-r--r-- | intf/misctypes.mli | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/intf/misctypes.mli b/intf/misctypes.mli index 7d9599032..91fdf3829 100644 --- a/intf/misctypes.mli +++ b/intf/misctypes.mli @@ -89,3 +89,8 @@ type 'a or_by_notation = (* NB: the last string in [ByNotation] is actually a [Notation.delimiters], but this formulation avoids a useless dependency. *) + + +(** Kinds of modules *) + +type module_kind = Module | ModType | ModAny |