aboutsummaryrefslogtreecommitdiffhomepage
path: root/library
diff options
context:
space:
mode:
Diffstat (limited to 'library')
-rw-r--r--library/assumptions.ml4
-rw-r--r--library/declare.ml2
-rw-r--r--library/declaremods.ml2
-rw-r--r--library/global.ml12
-rw-r--r--library/global.mli2
-rw-r--r--library/globnames.ml10
-rw-r--r--library/lib.ml10
-rw-r--r--library/libnames.ml2
-rw-r--r--library/nameops.ml2
-rw-r--r--library/nameops.mli2
10 files changed, 24 insertions, 24 deletions
diff --git a/library/assumptions.ml b/library/assumptions.ml
index 1f6c8eeeb..84e870499 100644
--- a/library/assumptions.ml
+++ b/library/assumptions.ml
@@ -60,12 +60,12 @@ let modcache = ref (MPmap.empty : structure_body MPmap.t)
let rec search_mod_label lab = function
| [] -> raise Not_found
- | (l, SFBmodule mb) :: _ when eq_label l lab -> mb
+ | (l, SFBmodule mb) :: _ when Label.equal l lab -> mb
| _ :: fields -> search_mod_label lab fields
let rec search_cst_label lab = function
| [] -> raise Not_found
- | (l, SFBconst cb) :: _ when eq_label l lab -> cb
+ | (l, SFBconst cb) :: _ when Label.equal l lab -> cb
| _ :: fields -> search_cst_label lab fields
let rec lookup_module_in_impl mp =
diff --git a/library/declare.ml b/library/declare.ml
index 015fc9894..20e5bdddc 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -117,7 +117,7 @@ let open_constant i ((sp,kn),_) =
Nametab.push (Nametab.Exactly i) sp (ConstRef con)
let exists_name id =
- variable_exists id or Global.exists_objlabel (label_of_id id)
+ variable_exists id or Global.exists_objlabel (Label.of_id id)
let check_exists sp =
let id = basename sp in
diff --git a/library/declaremods.ml b/library/declaremods.ml
index 10b04c588..763aa5ffd 100644
--- a/library/declaremods.ml
+++ b/library/declaremods.ml
@@ -440,7 +440,7 @@ let rec replace_module_object idl (mbids,mp,lib_stack) (mbids2,mp2,objs) mp1 =
if not (String.equal (object_tag obj) "MODULE") then anomaly "MODULE expected!";
let substobjs = match idl with
| [] ->
- let mp' = MPdot(mp, label_of_id id) in
+ let mp' = MPdot(mp, Label.of_id id) in
mbids, mp', subst_objects (map_mp mp1 mp' empty_delta_resolver) objs
| _ ->
replace_module_object idl (out_module obj) (mbids2,mp2,objs) mp
diff --git a/library/global.ml b/library/global.ml
index c2bd55128..f56cb7d61 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -46,7 +46,7 @@ let push_named_def d =
let add_thing add dir id thing =
- let kn, newenv = add dir (label_of_id id) thing !global_env in
+ let kn, newenv = add dir (Label.of_id id) thing !global_env in
global_env := newenv;
kn
@@ -56,7 +56,7 @@ let add_modtype x y inl = add_thing (fun _ x y -> add_modtype x y inl) () x y
let add_module id me inl =
- let l = label_of_id id in
+ let l = Label.of_id id in
let mp,resolve,new_env = add_module l me inl !global_env in
global_env := new_env;
mp,resolve
@@ -72,13 +72,13 @@ let add_include me is_module inl =
resolve
let start_module id =
- let l = label_of_id id in
+ let l = Label.of_id id in
let mp,newenv = start_module l !global_env in
global_env := newenv;
mp
let end_module fs id mtyo =
- let l = label_of_id id in
+ let l = Label.of_id id in
let mp,resolve,newenv = end_module l mtyo !global_env in
Summary.unfreeze_summaries fs;
global_env := newenv;
@@ -92,13 +92,13 @@ let add_module_parameter mbid mte inl =
let start_modtype id =
- let l = label_of_id id in
+ let l = Label.of_id id in
let mp,newenv = start_modtype l !global_env in
global_env := newenv;
mp
let end_modtype fs id =
- let l = label_of_id id in
+ let l = Label.of_id id in
let kn,newenv = end_modtype l !global_env in
Summary.unfreeze_summaries fs;
global_env := newenv;
diff --git a/library/global.mli b/library/global.mli
index dac230a44..d49dd836b 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -87,7 +87,7 @@ val lookup_module : module_path -> module_body
val lookup_modtype : module_path -> module_type_body
val constant_of_delta_kn : kernel_name -> constant
val mind_of_delta_kn : kernel_name -> mutual_inductive
-val exists_objlabel : label -> bool
+val exists_objlabel : Label.t -> bool
(** Compiled modules *)
val start_library : Dir_path.t -> module_path
diff --git a/library/globnames.ml b/library/globnames.ml
index efc46a7ac..c37e370a3 100644
--- a/library/globnames.ml
+++ b/library/globnames.ml
@@ -138,9 +138,9 @@ let constr_of_global_or_constr = function
(** {6 Temporary function to brutally form kernel names from section paths } *)
-let encode_mind dir id = make_mind (MPfile dir) Dir_path.empty (label_of_id id)
+let encode_mind dir id = make_mind (MPfile dir) Dir_path.empty (Label.of_id id)
-let encode_con dir id = make_con (MPfile dir) Dir_path.empty (label_of_id id)
+let encode_con dir id = make_con (MPfile dir) Dir_path.empty (Label.of_id id)
let decode_mind kn =
let rec dir_of_mp = function
@@ -149,18 +149,18 @@ let decode_mind kn =
let _,_,dp = repr_mbid mbid in
let id = id_of_mbid mbid in
id::(Dir_path.repr dp)
- | MPdot(mp,l) -> (id_of_label l)::(dir_of_mp mp)
+ | MPdot(mp,l) -> (Label.to_id l)::(dir_of_mp mp)
in
let mp,sec_dir,l = repr_mind kn in
if (Dir_path.repr sec_dir) = [] then
- (Dir_path.make (dir_of_mp mp)),id_of_label l
+ (Dir_path.make (dir_of_mp mp)),Label.to_id l
else
anomaly "Section part should be empty!"
let decode_con kn =
let mp,sec_dir,l = repr_con kn in
match mp,(Dir_path.repr sec_dir) with
- MPfile dir,[] -> (dir,id_of_label l)
+ MPfile dir,[] -> (dir,Label.to_id l)
| _ , [] -> anomaly "MPfile expected!"
| _ -> anomaly "Section part should be empty!"
diff --git a/library/lib.ml b/library/lib.ml
index ed64b1f40..9ac9b7c71 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -61,7 +61,7 @@ let classify_segment seg =
let rec clean ((substl,keepl,anticipl) as acc) = function
| (_,CompilingLibrary _) :: _ | [] -> acc
| ((sp,kn),Leaf o) :: stk ->
- let id = Names.id_of_label (Names.label kn) in
+ let id = Names.Label.to_id (Names.label kn) in
(match classify_object o with
| Dispose -> clean acc stk
| Keep o' ->
@@ -136,11 +136,11 @@ let current_prefix () = snd !path_prefix
let make_kn id =
let mp,dir = current_prefix () in
- Names.make_kn mp dir (Names.label_of_id id)
+ Names.make_kn mp dir (Names.Label.of_id id)
let make_con id =
let mp,dir = current_prefix () in
- Names.make_con mp dir (Names.label_of_id id)
+ Names.make_con mp dir (Names.Label.of_id id)
let make_oname id = make_path id, make_kn id
@@ -657,7 +657,7 @@ let rec split_mp mp =
| Names.MPfile dp -> dp, Names.Dir_path.empty
| Names.MPdot (prfx, lbl) ->
let mprec, dprec = split_mp prfx in
- mprec, Names.Dir_path.make (Names.Id.of_string (Names.string_of_label lbl) :: (Names.Dir_path.repr dprec))
+ mprec, Names.Dir_path.make (Names.Id.of_string (Names.Label.to_string lbl) :: (Names.Dir_path.repr dprec))
| Names.MPbound mbid -> let (_, id, dp) = Names.repr_mbid mbid in library_dp(), Names.Dir_path.make [id]
let split_modpath mp =
@@ -666,7 +666,7 @@ let split_modpath mp =
| Names.MPbound mbid ->
library_dp (), [Names.id_of_mbid mbid]
| Names.MPdot (mp,l) -> let (mp', lab) = aux mp in
- (mp', Names.id_of_label l :: lab)
+ (mp', Names.Label.to_id l :: lab)
in
let (mp, l) = aux mp in
mp, l
diff --git a/library/libnames.ml b/library/libnames.ml
index 8e026d8c2..7680e5248 100644
--- a/library/libnames.ml
+++ b/library/libnames.ml
@@ -151,7 +151,7 @@ type object_name = full_path * kernel_name
type object_prefix = Dir_path.t * (module_path * Dir_path.t)
let make_oname (dirpath,(mp,dir)) id =
- make_path dirpath id, make_kn mp dir (label_of_id id)
+ make_path dirpath id, make_kn mp dir (Label.of_id id)
(* to this type are mapped Dir_path.t's in the nametab *)
type global_dir_reference =
diff --git a/library/nameops.ml b/library/nameops.ml
index 361a53d6b..a8803e7a5 100644
--- a/library/nameops.ml
+++ b/library/nameops.ml
@@ -136,7 +136,7 @@ let name_fold_map f e = function
| Name id -> let (e,id) = f e id in (e,Name id)
| Anonymous -> e,Anonymous
-let pr_lab l = str (string_of_label l)
+let pr_lab l = str (Label.to_string l)
let default_library = Names.Dir_path.initial (* = ["Top"] *)
diff --git a/library/nameops.mli b/library/nameops.mli
index 6e9bde839..0f71d28a1 100644
--- a/library/nameops.mli
+++ b/library/nameops.mli
@@ -36,7 +36,7 @@ val name_app : (Id.t -> Id.t) -> name -> name
val name_fold_map : ('a -> Id.t -> 'a * Id.t) -> 'a -> name -> 'a * name
-val pr_lab : label -> Pp.std_ppcmds
+val pr_lab : Label.t -> Pp.std_ppcmds
(** some preset paths *)