From ea24fed3a1a91f945d0cce380d0ea1a9156e735e Mon Sep 17 00:00:00 2001
From: Jasper Hugunin <jasperh@cs.washington.edu>
Date: Tue, 24 Apr 2018 21:36:59 -0700
Subject: Remove DirClosedSection.

This has been around for at least 16 years, with the comment
"this won't last long I hope".
https://github.com/coq/coq/commit/12965209478bd99dfbe57f07d5b525e51b903f22#diff-1a3a6f7bd5b2cf1bc6dd43ee04bbc3eaR112
---
 printing/prettyp.ml | 1 -
 1 file changed, 1 deletion(-)

(limited to 'printing')

diff --git a/printing/prettyp.ml b/printing/prettyp.ml
index 1f17d844f..9c7408596 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 ->
-- 
cgit v1.2.3