diff options
| -rw-r--r-- | library/lib.ml | 4 | ||||
| -rw-r--r-- | library/libnames.ml | 3 | ||||
| -rw-r--r-- | library/libnames.mli | 2 | ||||
| -rw-r--r-- | library/nametab.ml | 1 | ||||
| -rw-r--r-- | printing/prettyp.ml | 1 |
5 files changed, 1 insertions, 10 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 = 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 -> |