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

1 files changed, 5 insertions, 6 deletions

diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml
index d9b839e857..23a8bf20a3 100644
--- a/vernac/indschemes.ml
+++ b/vernac/indschemes.ml
@@ -27,7 +27,6 @@ open Inductive
 open Indrec
 open Declare
 open Libnames
-open Globnames
 open Goptions
 open Nameops
 open Termops
@@ -376,7 +375,7 @@ requested
               | InSet -> recs ^ "_nodep"
               | InType -> recs ^ "t_nodep")
         ) in
-        let newid = add_suffix (Nametab.basename_of_global (IndRef ind)) suffix in
+        let newid = add_suffix (Nametab.basename_of_global (GlobRef.IndRef ind)) suffix in
         let newref = CAst.make newid in
           ((newref,isdep,ind,z)::l1),l2
       in
@@ -394,7 +393,7 @@ let do_mutual_induction_scheme ?(force_mutual=false) lnamedepindsort =
        let evd, indu, inst =
 	 match inst with
 	 | None ->
-            let _, ctx = Typeops.type_of_global_in_context env0 (IndRef ind) in
+            let _, ctx = Typeops.type_of_global_in_context env0 (GlobRef.IndRef ind) in
             let u, ctx = UnivGen.fresh_instance_from ctx None in
             let evd = Evd.from_ctx (UState.of_context_set ctx) in
 	      evd, (ind,u), Some u
@@ -408,14 +407,14 @@ let do_mutual_induction_scheme ?(force_mutual=false) lnamedepindsort =
     (* NB: build_mutual_induction_scheme forces nonempty list of mutual inductives
        (force_mutual is about the generated schemes) *)
     let _,_,ind,_ = List.hd lnamedepindsort in
-    Global.is_polymorphic (IndRef ind)
+    Global.is_polymorphic (GlobRef.IndRef ind)
   in
   let declare decl fi lrecref =
     let decltype = Retyping.get_type_of env0 sigma (EConstr.of_constr decl) in
     let decltype = EConstr.to_constr sigma decltype in
     let proof_output = Future.from_val ((decl,Univ.ContextSet.empty),Evd.empty_side_effects) in
     let cst = define ~poly fi sigma proof_output (Some decltype) in
-    ConstRef cst :: lrecref
+    GlobRef.ConstRef cst :: lrecref
   in
   let _ = List.fold_right2 declare listdecl lrecnames [] in
   fixpoint_message None lrecnames
@@ -542,7 +541,7 @@ let do_combined_scheme name schemes =
      polymorphism of the inductive block). In that case if they want
      some other polymorphism they can also manually define the
      combined scheme. *)
-  let poly = Global.is_polymorphic (ConstRef (List.hd csts)) in
+  let poly = Global.is_polymorphic (GlobRef.ConstRef (List.hd csts)) in
   ignore (define ~poly name.v sigma proof_output (Some typ));
   fixpoint_message None [name.v]