aboutsummaryrefslogtreecommitdiff
path: root/library
diff options
context:
space:
mode:
Diffstat (limited to 'library')
-rw-r--r--library/declaremods.ml8
-rw-r--r--library/lib.ml2
-rw-r--r--library/libnames.ml14
-rw-r--r--library/libnames.mli10
-rw-r--r--library/nametab.ml38
-rw-r--r--library/nametab.mli22
6 files changed, 51 insertions, 43 deletions
diff --git a/library/declaremods.ml b/library/declaremods.ml
index e01a99f731..f4edbe36bb 100644
--- a/library/declaremods.ml
+++ b/library/declaremods.ml
@@ -185,7 +185,7 @@ let consistency_checks exists dir dirinfo =
user_err ~hdr:"consistency_checks"
(DirPath.print dir ++ str " should already exist!")
in
- assert (eq_global_dir_reference globref dirinfo)
+ assert (Nametab.GlobDirRef.equal globref dirinfo)
else
if Nametab.exists_dir dir then
user_err ~hdr:"consistency_checks"
@@ -198,7 +198,7 @@ let compute_visibility exists i =
let do_module exists iter_objects i obj_dir obj_mp sobjs kobjs =
let prefix = { obj_dir ; obj_mp; obj_sec = DirPath.empty } in
- let dirinfo = DirModule prefix in
+ let dirinfo = Nametab.GlobDirRef.DirModule prefix in
consistency_checks exists obj_dir dirinfo;
Nametab.push_dir (compute_visibility exists i) obj_dir dirinfo;
ModSubstObjs.set obj_mp sobjs;
@@ -605,7 +605,7 @@ let start_module interp_modast export id args res fs =
let () = Global.push_context_set true cst in
openmod_info := { cur_typ = res_entry_o; cur_typs = subtyps };
let prefix = Lib.start_module export id mp fs in
- Nametab.push_dir (Nametab.Until 1) (prefix.obj_dir) (DirOpenModule prefix);
+ Nametab.(push_dir (Until 1) (prefix.obj_dir) (GlobDirRef.DirOpenModule prefix));
mp
let end_module () =
@@ -723,7 +723,7 @@ let start_modtype interp_modast id args mtys fs =
let () = Global.push_context_set true cst in
openmodtype_info := sub_mty_l;
let prefix = Lib.start_modtype id mp fs in
- Nametab.push_dir (Nametab.Until 1) (prefix.obj_dir) (DirOpenModtype prefix);
+ Nametab.(push_dir (Until 1) (prefix.obj_dir) (GlobDirRef.DirOpenModtype prefix));
mp
let end_modtype () =
diff --git a/library/lib.ml b/library/lib.ml
index 1acc8fd8fd..762a2e0567 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -551,7 +551,7 @@ let open_section id =
let fs = Summary.freeze_summaries ~marshallable:`No in
add_entry (make_oname id) (OpenedSection (prefix, fs));
(*Pushed for the lifetime of the section: removed by unfrozing the summary*)
- Nametab.push_dir (Nametab.Until 1) obj_dir (DirOpenSection prefix);
+ Nametab.(push_dir (Until 1) obj_dir (GlobDirRef.DirOpenSection prefix));
lib_state := { !lib_state with path_prefix = prefix };
add_section ()
diff --git a/library/libnames.ml b/library/libnames.ml
index f6fc5ed4b7..d2c96d4163 100644
--- a/library/libnames.ml
+++ b/library/libnames.ml
@@ -168,25 +168,11 @@ type object_prefix = {
obj_sec : DirPath.t;
}
-(* to this type are mapped DirPath.t's in the nametab *)
-type global_dir_reference =
- | DirOpenModule of object_prefix
- | DirOpenModtype of object_prefix
- | DirOpenSection of object_prefix
- | DirModule of object_prefix
-
let eq_op op1 op2 =
DirPath.equal op1.obj_dir op2.obj_dir &&
DirPath.equal op1.obj_sec op2.obj_sec &&
ModPath.equal op1.obj_mp op2.obj_mp
-let eq_global_dir_reference r1 r2 = match r1, r2 with
-| DirOpenModule op1, DirOpenModule op2 -> eq_op op1 op2
-| DirOpenModtype op1, DirOpenModtype op2 -> eq_op op1 op2
-| DirOpenSection op1, DirOpenSection op2 -> eq_op op1 op2
-| DirModule op1, DirModule op2 -> eq_op op1 op2
-| _ -> false
-
(* Default paths *)
let default_library = Names.DirPath.initial (* = ["Top"] *)
diff --git a/library/libnames.mli b/library/libnames.mli
index 9d75ec6e40..56368fd08c 100644
--- a/library/libnames.mli
+++ b/library/libnames.mli
@@ -110,16 +110,6 @@ type object_prefix = {
val eq_op : object_prefix -> object_prefix -> bool
-(** to this type are mapped [DirPath.t]'s in the nametab *)
-type global_dir_reference =
- | DirOpenModule of object_prefix
- | DirOpenModtype of object_prefix
- | DirOpenSection of object_prefix
- | DirModule of object_prefix
-
-val eq_global_dir_reference :
- global_dir_reference -> global_dir_reference -> bool
-
(** {6 ... } *)
(** some preset paths *)
diff --git a/library/nametab.ml b/library/nametab.ml
index 06ace373c3..7f94357a8b 100644
--- a/library/nametab.ml
+++ b/library/nametab.ml
@@ -15,6 +15,28 @@ open Names
open Libnames
open Globnames
+(* to this type are mapped DirPath.t's in the nametab *)
+module GlobDirRef = struct
+ type t =
+ | DirOpenModule of object_prefix
+ | DirOpenModtype of object_prefix
+ | DirOpenSection of object_prefix
+ | DirModule of object_prefix
+
+ let equal r1 r2 = match r1, r2 with
+ | DirOpenModule op1, DirOpenModule op2 -> eq_op op1 op2
+ | DirOpenModtype op1, DirOpenModtype op2 -> eq_op op1 op2
+ | DirOpenSection op1, DirOpenSection op2 -> eq_op op1 op2
+ | DirModule op1, DirModule op2 -> eq_op op1 op2
+ | _ -> false
+
+end
+
+type global_dir_reference = GlobDirRef.t
+[@@ocaml.deprecated "Use [GlobDirRef.t]"]
+
+let eq_global_dir_reference = GlobDirRef.equal
+[@@ocaml.deprecated "Use [GlobDirRef.equal]"]
exception GlobalizationError of qualid
@@ -295,13 +317,7 @@ struct
| id :: l -> (id, l)
end
-module GlobDir =
-struct
- type t = global_dir_reference
- let equal = eq_global_dir_reference
-end
-
-module DirTab = Make(DirPath')(GlobDir)
+module DirTab = Make(DirPath')(GlobDirRef)
(* If we have a (closed) module M having a submodule N, than N does not
have the entry in [the_dirtab]. *)
@@ -390,7 +406,7 @@ let push_modtype vis sp kn =
let push_dir vis dir dir_ref =
the_dirtab := DirTab.push vis dir dir_ref !the_dirtab;
match dir_ref with
- | DirModule { obj_mp; _ } -> the_modrevtab := MPmap.add obj_mp dir !the_modrevtab
+ | GlobDirRef.DirModule { obj_mp; _ } -> the_modrevtab := MPmap.add obj_mp dir !the_modrevtab
| _ -> ()
(* This is for global universe names *)
@@ -424,17 +440,17 @@ let locate_dir qid = DirTab.locate qid !the_dirtab
let locate_module qid =
match locate_dir qid with
- | DirModule { obj_mp ; _} -> obj_mp
+ | GlobDirRef.DirModule { obj_mp ; _} -> obj_mp
| _ -> raise Not_found
let full_name_module qid =
match locate_dir qid with
- | DirModule { obj_dir ; _} -> obj_dir
+ | GlobDirRef.DirModule { obj_dir ; _} -> obj_dir
| _ -> raise Not_found
let locate_section qid =
match locate_dir qid with
- | DirOpenSection { obj_dir; _ } -> obj_dir
+ | GlobDirRef.DirOpenSection { obj_dir; _ } -> obj_dir
| _ -> raise Not_found
let locate_all qid =
diff --git a/library/nametab.mli b/library/nametab.mli
index 1c3322bfb1..b71bc77cbb 100644
--- a/library/nametab.mli
+++ b/library/nametab.mli
@@ -57,6 +57,22 @@ open Globnames
*)
+(** to this type are mapped [DirPath.t]'s in the nametab *)
+module GlobDirRef : sig
+ type t =
+ | DirOpenModule of object_prefix
+ | DirOpenModtype of object_prefix
+ | DirOpenSection of object_prefix
+ | DirModule of object_prefix
+ val equal : t -> t -> bool
+end
+
+type global_dir_reference = GlobDirRef.t
+[@@ocaml.deprecated "Use [GlobDirRef.t]"]
+
+val eq_global_dir_reference :
+ GlobDirRef.t -> GlobDirRef.t -> bool
+[@@ocaml.deprecated "Use [GlobDirRef.equal]"]
exception GlobalizationError of qualid
@@ -79,7 +95,7 @@ val map_visibility : (int -> int) -> visibility -> visibility
val push : visibility -> full_path -> GlobRef.t -> unit
val push_modtype : visibility -> full_path -> ModPath.t -> unit
-val push_dir : visibility -> DirPath.t -> global_dir_reference -> unit
+val push_dir : visibility -> DirPath.t -> GlobDirRef.t -> unit
val push_syndef : visibility -> full_path -> syndef_name -> unit
type universe_id = DirPath.t * int
@@ -98,7 +114,7 @@ val locate_extended : qualid -> extended_global_reference
val locate_constant : qualid -> Constant.t
val locate_syndef : qualid -> syndef_name
val locate_modtype : qualid -> ModPath.t
-val locate_dir : qualid -> global_dir_reference
+val locate_dir : qualid -> GlobDirRef.t
val locate_module : qualid -> ModPath.t
val locate_section : qualid -> DirPath.t
val locate_universe : qualid -> universe_id
@@ -115,7 +131,7 @@ val global_inductive : qualid -> inductive
val locate_all : qualid -> GlobRef.t list
val locate_extended_all : qualid -> extended_global_reference list
-val locate_extended_all_dir : qualid -> global_dir_reference list
+val locate_extended_all_dir : qualid -> GlobDirRef.t list
val locate_extended_all_modtype : qualid -> ModPath.t list
(** Mapping a full path to a global reference *)
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 14:23:49 +0000