diff options
| author | Emilio Jesus Gallego Arias | 2019-06-21 22:50:08 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-07-08 15:59:10 +0200 |
| commit | c51fb2fae0e196012de47203b8a71c61720d6c5c (patch) | |
| tree | e49c2d38b6c841dc6514944750d21ed08ab94bce /library/lib.ml | |
| parent | 437063a0c745094c5693d1c5abba46ce375d69c6 (diff) | |
[api] Deprecate GlobRef constructors.
Not pretty, but it had to be done some day, as `Globnames` seems to be
on the way out.
I have taken the opportunity to reduce the number of `open` in the
codebase.
The qualified style would indeed allow us to use a bit nicer names
`GlobRef.Inductive` instead of `IndRef`, etc... once we have the
tooling to do large-scale refactoring that could be tried.
Diffstat (limited to 'library/lib.ml')
| -rw-r--r-- | library/lib.ml | 13 |
1 files changed, 6 insertions, 7 deletions
diff --git a/library/lib.ml b/library/lib.ml index 576e23c4f5..d461644d56 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -13,7 +13,6 @@ open CErrors open Util open Names open Libnames -open Globnames open Libobject open Context.Named.Declaration @@ -549,7 +548,7 @@ let empty_segment = { abstr_uctx = Univ.AUContext.empty; } -let section_segment_of_reference = function +let section_segment_of_reference = let open GlobRef in function | ConstRef c -> section_segment_of_constant c | IndRef (kn,_) | ConstructRef ((kn,_),_) -> section_segment_of_mutual_inductive kn @@ -558,7 +557,7 @@ let section_segment_of_reference = function let variable_section_segment_of_reference gr = (section_segment_of_reference gr).abstr_ctx -let section_instance = function +let section_instance = let open GlobRef in function | VarRef id -> let eq = function | Variable {id=id'} -> Names.Id.equal id id' @@ -647,7 +646,7 @@ let init () = (* Misc *) -let mp_of_global = function +let mp_of_global = let open GlobRef in function | VarRef id -> !lib_state.path_prefix.Nametab.obj_mp | ConstRef cst -> Names.Constant.modpath cst | IndRef ind -> Names.ind_modpath ind @@ -666,12 +665,12 @@ let rec split_modpath = function (dp, Names.Label.to_id l :: ids) let library_part = function - |VarRef id -> library_dp () - |ref -> dp_of_mp (mp_of_global ref) + | GlobRef.VarRef id -> library_dp () + | ref -> dp_of_mp (mp_of_global ref) let discharge_proj_repr = Projection.Repr.map_npars (fun mind npars -> - if not (is_in_section (IndRef (mind,0))) then mind, npars + if not (is_in_section (GlobRef.IndRef (mind,0))) then mind, npars else let modlist = replacement_context () in let _, newpars = Mindmap.find mind (snd modlist) in mind, npars + Array.length newpars) |