diff options
Diffstat (limited to 'intf')
| -rw-r--r-- | intf/vernacexpr.mli | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli index 37f25e0ac4..d4d30dce84 100644 --- a/intf/vernacexpr.mli +++ b/intf/vernacexpr.mli @@ -42,6 +42,7 @@ type printable = | PrintModules | PrintModule of reference | PrintModuleType of reference + | PrintNamespace of dir_path | PrintMLLoadPath | PrintMLModules | PrintName of reference or_by_notation |