Merge PR #10498: [api] Deprecate GlobRef constructors.

Reviewed-by: SkySkimmer
Ack-by: ppedrot

6 files changed, 43 insertions, 40 deletions

diff --git a/library/coqlib.ml b/library/coqlib.ml
index 7cd2e50274..b1e4ef2b00 100644
--- a/library/coqlib.ml
+++ b/library/coqlib.ml
@@ -13,7 +13,6 @@ open Util
 open Pp
 open Names
 open Libnames
-open Globnames
 
 let make_dir l = DirPath.make (List.rev_map Id.of_string l)
 
@@ -46,7 +45,7 @@ let has_ref s = CString.Map.mem s !table
 
 let check_ind_ref s ind =
   match CString.Map.find s !table with
-  | IndRef r -> eq_ind r ind
+  | GlobRef.IndRef r -> eq_ind r ind
   | _ -> false
   | exception Not_found -> false
 
@@ -157,32 +156,32 @@ let type_of_id = Constant.make2 datatypes_module @@ Label.make "IDProp"
 let nat_kn = MutInd.make2 datatypes_module @@ Label.make "nat"
 let nat_path = Libnames.make_path (make_dir datatypes_module_name) (Id.of_string "nat")
 
-let glob_nat = IndRef (nat_kn,0)
+let glob_nat = GlobRef.IndRef (nat_kn,0)
 
 let path_of_O = ((nat_kn,0),1)
 let path_of_S = ((nat_kn,0),2)
-let glob_O = ConstructRef path_of_O
-let glob_S = ConstructRef path_of_S
+let glob_O = GlobRef.ConstructRef path_of_O
+let glob_S = GlobRef.ConstructRef path_of_S
 
 (** Booleans *)
 let bool_kn = MutInd.make2 datatypes_module @@ Label.make "bool"
 
-let glob_bool = IndRef (bool_kn,0)
+let glob_bool = GlobRef.IndRef (bool_kn,0)
 
 let path_of_true = ((bool_kn,0),1)
 let path_of_false = ((bool_kn,0),2)
-let glob_true  = ConstructRef path_of_true
-let glob_false  = ConstructRef path_of_false
+let glob_true  = GlobRef.ConstructRef path_of_true
+let glob_false  = GlobRef.ConstructRef path_of_false
 
 (** Equality *)
 let eq_kn = MutInd.make2 logic_module @@ Label.make "eq"
-let glob_eq = IndRef (eq_kn,0)
+let glob_eq = GlobRef.IndRef (eq_kn,0)
 
 let identity_kn = MutInd.make2 datatypes_module @@ Label.make "identity"
-let glob_identity = IndRef (identity_kn,0)
+let glob_identity = GlobRef.IndRef (identity_kn,0)
 
 let jmeq_kn = MutInd.make2 jmeq_module @@ Label.make "JMeq"
-let glob_jmeq = IndRef (jmeq_kn,0)
+let glob_jmeq = GlobRef.IndRef (jmeq_kn,0)
 
 (* Sigma data *)
 type coq_sigma_data = {
diff --git a/library/globnames.ml b/library/globnames.ml
index 71447c4b81..acb05f9ac0 100644
--- a/library/globnames.ml
+++ b/library/globnames.ml
@@ -12,12 +12,14 @@ open Names
 open Constr
 open Mod_subst
 
-(*s Global reference is a kernel side type for all references together *)
 type global_reference = GlobRef.t =
-  | VarRef of variable           (** A reference to the section-context. *)
-  | ConstRef of Constant.t       (** A reference to the environment. *)
-  | IndRef of inductive          (** A reference to an inductive type. *)
-  | ConstructRef of constructor  (** A reference to a constructor of an inductive type. *)
+  | VarRef of variable     [@ocaml.deprecated "Use Names.GlobRef.VarRef"]
+  | ConstRef of Constant.t [@ocaml.deprecated "Use Names.GlobRef.ConstRef"]
+  | IndRef of inductive    [@ocaml.deprecated "Use Names.GlobRef.IndRef"]
+  | ConstructRef of constructor [@ocaml.deprecated "Use Names.GlobRef.ConstructRef"]
+[@@ocaml.deprecated "Use Names.GlobRef.t"]
+
+open GlobRef
 
 let isVarRef = function VarRef _ -> true | _ -> false
 let isConstRef = function ConstRef _ -> true | _ -> false
@@ -90,7 +92,7 @@ let printable_constr_of_global = function
 type syndef_name = KerName.t
 
 type extended_global_reference =
-  | TrueGlobal of global_reference
+  | TrueGlobal of GlobRef.t
   | SynDef of syndef_name
 
 (* We order [extended_global_reference] via their user part
@@ -122,6 +124,6 @@ module ExtRefOrdered = struct
 
 end
 
-type global_reference_or_constr = 
-  | IsGlobal of global_reference
+type global_reference_or_constr =
+  | IsGlobal of GlobRef.t
   | IsConstr of constr
diff --git a/library/globnames.mli b/library/globnames.mli
index 547755b088..fc0de96e36 100644
--- a/library/globnames.mli
+++ b/library/globnames.mli
@@ -12,12 +12,11 @@ open Names
 open Constr
 open Mod_subst
 
-(** {6 Global reference is a kernel side type for all references together } *)
 type global_reference = GlobRef.t =
-  | VarRef of variable           (** A reference to the section-context. *)
-  | ConstRef of Constant.t       (** A reference to the environment. *)
-  | IndRef of inductive          (** A reference to an inductive type. *)
-  | ConstructRef of constructor  (** A reference to a constructor of an inductive type. *)
+  | VarRef of variable     [@ocaml.deprecated "Use Names.GlobRef.VarRef"]
+  | ConstRef of Constant.t [@ocaml.deprecated "Use Names.GlobRef.ConstRef"]
+  | IndRef of inductive    [@ocaml.deprecated "Use Names.GlobRef.IndRef"]
+  | ConstructRef of constructor [@ocaml.deprecated "Use Names.GlobRef.ConstructRef"]
 [@@ocaml.deprecated "Use Names.GlobRef.t"]
 
 val isVarRef : GlobRef.t -> bool
diff --git a/library/keys.ml b/library/keys.ml
index 30ecc9dfdb..9964992433 100644
--- a/library/keys.ml
+++ b/library/keys.ml
@@ -94,7 +94,7 @@ let subst_keys (subst,(k,k')) =
   (subst_key subst k, subst_key subst k')
 
 let discharge_key = function
-  | KGlob (VarRef _ as g) when Lib.is_in_section g -> None
+  | KGlob (GlobRef.VarRef _ as g) when Lib.is_in_section g -> None
   | x -> Some x
 
 let discharge_keys (_,(k,k')) =
@@ -114,16 +114,15 @@ let declare_equiv_keys ref ref' =
   Lib.add_anonymous_leaf (inKeys (ref,ref'))
 
 let constr_key kind c =
-  let open Globnames in 
-  try 
-    let rec aux k = 
+  try
+    let rec aux k =
       match kind k with
-      | Const (c, _) -> KGlob (ConstRef c)
-      | Ind (i, u) -> KGlob (IndRef i)
-      | Construct (c,u) -> KGlob (ConstructRef c)
-      | Var id -> KGlob (VarRef id)
+      | Const (c, _) -> KGlob (GlobRef.ConstRef c)
+      | Ind (i, u) -> KGlob (GlobRef.IndRef i)
+      | Construct (c,u) -> KGlob (GlobRef.ConstructRef c)
+      | Var id -> KGlob (GlobRef.VarRef id)
       | App (f, _) -> aux f
-      | Proj (p, _) -> KGlob (ConstRef (Projection.constant p))
+      | Proj (p, _) -> KGlob (GlobRef.ConstRef (Projection.constant p))
       | Cast (p, _, _) -> aux p
       | Lambda _ -> KLam 
       | Prod _ -> KProd
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)
diff --git a/library/nametab.ml b/library/nametab.ml
index 71ee7a6d5a..aed7d08ac1 100644
--- a/library/nametab.ml
+++ b/library/nametab.ml
@@ -392,6 +392,7 @@ let push_xref visibility sp xref =
     | _ ->
 	begin
 	  if ExtRefTab.exists sp !the_ccitab then
+            let open GlobRef in
 	    match ExtRefTab.find sp !the_ccitab with
 	      | TrueGlobal( ConstRef _) | TrueGlobal( IndRef _) |
 		    TrueGlobal( ConstructRef _) as xref ->
@@ -483,6 +484,7 @@ let completion_canditates qualid =
 (* Derived functions *)
 
 let locate_constant qid =
+  let open GlobRef in
   match locate_extended qid with
     | TrueGlobal (ConstRef kn) -> kn
     | _ -> raise Not_found
@@ -517,6 +519,7 @@ let exists_universe kn = UnivTab.exists kn !the_univtab
 (* Reverse locate functions ***********************************************)
 
 let path_of_global ref =
+  let open GlobRef in
   match ref with
     | VarRef id -> make_path DirPath.empty id
     | _ -> Globrevtab.find (TrueGlobal ref) !the_globrevtab
@@ -542,6 +545,7 @@ let path_of_universe mp =
 (* Shortest qualid functions **********************************************)
 
 let shortest_qualid_of_global ?loc ctx ref =
+  let open GlobRef in
   match ref with
     | VarRef id -> make_qualid ?loc DirPath.empty id
     | _ ->
@@ -570,6 +574,7 @@ let pr_global_env env ref =
     if !Flags.debug then Feedback.msg_debug (Pp.str "pr_global_env not found"); raise e
 
 let global_inductive qid =
+  let open GlobRef in
   match global qid with
   | IndRef ind -> ind
   | ref ->