aboutsummaryrefslogtreecommitdiffhomepage
path: root/library
diff options
context:
space:
mode:
authorGravatar Jasper Hugunin <jasperh@cs.washington.edu>2018-04-24 21:36:59 -0700
committerGravatar Jasper Hugunin <jasperh@cs.washington.edu>2018-04-24 21:36:59 -0700
commitea24fed3a1a91f945d0cce380d0ea1a9156e735e (patch)
tree69be6177e5bae042f8a70ceaa6aee5e195991f8b /library
parent72d6d5e87759b62dcd9974c87bf59496d27e10b0 (diff)
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
Diffstat (limited to 'library')
-rw-r--r--library/lib.ml4
-rw-r--r--library/libnames.ml3
-rw-r--r--library/libnames.mli2
-rw-r--r--library/nametab.ml1
4 files changed, 1 insertions, 9 deletions
diff --git a/library/lib.ml b/library/lib.ml
index 543cb45bc..fde13d0e3 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -580,13 +580,11 @@ let close_section () =
in
let (secdecls,mark,before) = split_lib_at_opening oname in
lib_state := { !lib_state with lib_stk = before };
- let full_olddir = !lib_state.path_prefix.obj_dir in
pop_path_prefix ();
add_entry oname (ClosedSection (List.rev (mark::secdecls)));
let newdecls = List.map discharge_item secdecls in
Summary.unfreeze_summaries fs;
- List.iter (Option.iter (fun (id,o) -> add_discharged_leaf id o)) newdecls;
- Nametab.push_dir (Nametab.Until 1) full_olddir (DirClosedSection full_olddir)
+ List.iter (Option.iter (fun (id,o) -> add_discharged_leaf id o)) newdecls
(* State and initialization. *)
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 =
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
diff --git a/library/nametab.ml b/library/nametab.ml
index 2046bf758..995f44706 100644
--- a/library/nametab.ml
+++ b/library/nametab.ml
@@ -432,7 +432,6 @@ let full_name_module qid =
let locate_section qid =
match locate_dir qid with
| DirOpenSection { obj_dir; _ } -> obj_dir
- | DirClosedSection dir -> dir
| _ -> raise Not_found
let locate_all qid =