diff options
Diffstat (limited to 'printing')
| -rw-r--r-- | printing/prettyp.ml | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/printing/prettyp.ml b/printing/prettyp.ml index b95691031..185b1648c 100644 --- a/printing/prettyp.ml +++ b/printing/prettyp.ml @@ -376,7 +376,6 @@ let pr_located_qualid = function | DirOpenModtype { obj_dir ; _ } -> "Open Module Type", obj_dir | DirOpenSection { obj_dir ; _ } -> "Open Section", obj_dir | DirModule { obj_dir ; _ } -> "Module", obj_dir - | DirClosedSection dir -> "Closed Section", dir in str s ++ spc () ++ DirPath.print dir | ModuleType mp -> |