[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.

3 files changed, 15 insertions, 16 deletions

diff --git a/engine/namegen.ml b/engine/namegen.ml
index 77d45ce1e4..89c2fade62 100644
--- a/engine/namegen.ml
+++ b/engine/namegen.ml
@@ -24,7 +24,6 @@ open EConstr
 open Vars
 open Nameops
 open Libnames
-open Globnames
 open Context.Rel.Declaration
 
 module RelDecl = Context.Rel.Declaration
@@ -72,7 +71,7 @@ let is_imported_modpath = function
     in find_prefix (Lib.current_mp ())
   | _ -> false
 
-let is_imported_ref = function
+let is_imported_ref = let open GlobRef in function
   | VarRef _ -> false
   | IndRef (kn,_)
   | ConstructRef ((kn,_),_) ->
@@ -90,7 +89,7 @@ let is_global id =
 let is_constructor id =
   try
     match Nametab.locate (qualid_of_ident id) with
-      | ConstructRef _ -> true
+      | GlobRef.ConstructRef _ -> true
       | _ -> false
   with Not_found ->
     false
@@ -102,7 +101,7 @@ let is_section_variable id =
 (**********************************************************************)
 (* Generating "intuitive" names from its type *)
 
-let global_of_constr = function
+let global_of_constr = let open GlobRef in function
 | Const (c, _) -> ConstRef c
 | Ind (i, _) -> IndRef i
 | Construct (c, _) -> ConstructRef c
@@ -149,8 +148,8 @@ let hdchar env sigma c =
     | Cast (c,_,_) | App (c,_) -> hdrec k c
     | Proj (kn,_) -> lowercase_first_char (Label.to_id (Constant.label (Projection.constant kn)))
     | Const (kn,_) -> lowercase_first_char (Label.to_id (Constant.label kn))
-    | Ind (x,_) -> (try lowercase_first_char (Nametab.basename_of_global (IndRef x)) with Not_found when !Flags.in_debugger -> "zz")
-    | Construct (x,_) -> (try lowercase_first_char (Nametab.basename_of_global (ConstructRef x)) with Not_found when !Flags.in_debugger -> "zz")
+    | Ind (x,_) -> (try lowercase_first_char (Nametab.basename_of_global (GlobRef.IndRef x)) with Not_found when !Flags.in_debugger -> "zz")
+    | Construct (x,_) -> (try lowercase_first_char (Nametab.basename_of_global (GlobRef.ConstructRef x)) with Not_found when !Flags.in_debugger -> "zz")
     | Var id  -> lowercase_first_char id
     | Sort s -> sort_hdchar (ESorts.kind sigma s)
     | Rel n ->
diff --git a/engine/termops.ml b/engine/termops.ml
index 1ed2d93b3c..2ab2f60421 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -1058,7 +1058,7 @@ let is_section_variable id =
   with Not_found -> false
 
 let global_of_constr sigma c =
-  let open Globnames in
+  let open GlobRef in
   match EConstr.kind sigma c with
   | Const (c, u) -> ConstRef c, u
   | Ind (i, u) -> IndRef i, u
@@ -1067,7 +1067,7 @@ let global_of_constr sigma c =
   | _ -> raise Not_found
 
 let is_global sigma c t =
-  let open Globnames in
+  let open GlobRef in
   match c, EConstr.kind sigma t with
   | ConstRef c, Const (c', _) -> Constant.equal c c'
   | IndRef i, Ind (i', _) -> eq_ind i i'
@@ -1379,7 +1379,7 @@ let dependency_closure env sigma sign hyps =
     List.rev lh
 
 let global_app_of_constr sigma c =
-  let open Globnames in
+  let open GlobRef in
   match EConstr.kind sigma c with
   | Const (c, u) -> (ConstRef c, u), None
   | Ind (i, u) -> (IndRef i, u), None
diff --git a/engine/univGen.ml b/engine/univGen.ml
index a347bba188..b1ed3b2694 100644
--- a/engine/univGen.ml
+++ b/engine/univGen.ml
@@ -56,15 +56,15 @@ let fresh_global_instance ?loc ?names env gr =
   u, ctx
 
 let fresh_constant_instance env c =
-  let u, ctx = fresh_global_instance env (ConstRef c) in
+  let u, ctx = fresh_global_instance env (GlobRef.ConstRef c) in
   (c, u), ctx
 
 let fresh_inductive_instance env ind =
-  let u, ctx = fresh_global_instance env (IndRef ind) in
+  let u, ctx = fresh_global_instance env (GlobRef.IndRef ind) in
   (ind, u), ctx
 
 let fresh_constructor_instance env c =
-  let u, ctx = fresh_global_instance env (ConstructRef c) in
+  let u, ctx = fresh_global_instance env (GlobRef.ConstructRef c) in
   (c, u), ctx
 
 let fresh_global_instance ?loc ?names env gr =
@@ -84,10 +84,10 @@ let fresh_global_or_constr_instance env = function
 
 let global_of_constr c =
   match kind c with
-  | Const (c, u) -> ConstRef c, u
-  | Ind (i, u) -> IndRef i, u
-  | Construct (c, u) -> ConstructRef c, u
-  | Var id -> VarRef id, Instance.empty
+  | Const (c, u) -> GlobRef.ConstRef c, u
+  | Ind (i, u) -> GlobRef.IndRef i, u
+  | Construct (c, u) -> GlobRef.ConstructRef c, u
+  | Var id -> GlobRef.VarRef id, Instance.empty
   | _ -> raise Not_found
 
 let fresh_sort_in_family = function