diff options
Diffstat (limited to 'parsing/printmod.ml')
| -rw-r--r-- | parsing/printmod.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/parsing/printmod.ml b/parsing/printmod.ml index 596ce6b24..2ec914d6c 100644 --- a/parsing/printmod.ml +++ b/parsing/printmod.ml @@ -137,7 +137,7 @@ and print_modexpr locals mexpr = match mexpr with let rec printable_body dir = - let dir = dirpath_prefix dir in + let dir = pop_dirpath dir in dir = empty_dirpath || try match Nametab.locate_dir (qualid_of_dirpath dir) with |