From ea24fed3a1a91f945d0cce380d0ea1a9156e735e Mon Sep 17 00:00:00 2001 From: Jasper Hugunin 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.ml | 3 --- 1 file changed, 3 deletions(-) (limited to 'library/libnames.ml') diff --git a/library/libnames.ml b/library/libnames.ml index d84731322..4ceea480d 100644 --- a/library/libnames.ml +++ b/library/libnames.ml @@ -174,8 +174,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! *) let eq_op op1 op2 = DirPath.equal op1.obj_dir op2.obj_dir && @@ -187,7 +185,6 @@ let eq_global_dir_reference r1 r2 = match r1, r2 with | DirOpenModtype op1, DirOpenModtype op2 -> eq_op op1 op2 | DirOpenSection op1, DirOpenSection op2 -> eq_op op1 op2 | DirModule op1, DirModule op2 -> eq_op op1 op2 -| DirClosedSection dp1, DirClosedSection dp2 -> DirPath.equal dp1 dp2 | _ -> false type reference_r = -- cgit v1.2.3