diff options
Diffstat (limited to 'library')
| -rw-r--r-- | library/assumptions.ml | 4 | ||||
| -rw-r--r-- | library/declare.ml | 2 | ||||
| -rw-r--r-- | library/declaremods.ml | 2 | ||||
| -rw-r--r-- | library/global.ml | 12 | ||||
| -rw-r--r-- | library/global.mli | 2 | ||||
| -rw-r--r-- | library/globnames.ml | 10 | ||||
| -rw-r--r-- | library/lib.ml | 10 | ||||
| -rw-r--r-- | library/libnames.ml | 2 | ||||
| -rw-r--r-- | library/nameops.ml | 2 | ||||
| -rw-r--r-- | library/nameops.mli | 2 |
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 *) |