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
---
 library/libnames.mli | 2 --
 1 file changed, 2 deletions(-)

(limited to 'library/libnames.mli')

diff --git a/library/libnames.mli b/library/libnames.mli
index 9dad26129..81e5bc5b1 100644
--- a/library/libnames.mli
+++ b/library/libnames.mli
@@ -125,8 +125,6 @@ type global_dir_reference =
   | DirOpenModtype of object_prefix
   | DirOpenSection of object_prefix
   | DirModule of object_prefix
-  | DirClosedSection of DirPath.t
-      (** this won't last long I hope! *)
 
 val eq_global_dir_reference : 
   global_dir_reference -> global_dir_reference -> bool
-- 
cgit v1.2.3