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

9 files changed, 79 insertions, 86 deletions

diff --git a/plugins/extraction/common.ml b/plugins/extraction/common.ml
index 9abf212443..6c845a75b2 100644
--- a/plugins/extraction/common.ml
+++ b/plugins/extraction/common.ml
@@ -15,7 +15,6 @@ open ModPath
 open Namegen
 open Nameops
 open Libnames
-open Globnames
 open Table
 open Miniml
 open Mlutil
@@ -629,21 +628,21 @@ let check_extract_ascii () =
       | Haskell -> "Prelude.Char"
       | _ -> raise Not_found
     in
-    String.equal (find_custom (IndRef (ind_ascii, 0))) (char_type)
+    String.equal (find_custom (GlobRef.IndRef (ind_ascii, 0))) (char_type)
   with Not_found -> false
 
 let is_list_cons l =
- List.for_all (function MLcons (_,ConstructRef(_,_),[]) -> true | _ -> false) l
+ List.for_all (function MLcons (_,GlobRef.ConstructRef(_,_),[]) -> true | _ -> false) l
 
 let is_native_char = function
-  | MLcons(_,ConstructRef ((kn,0),1),l) ->
+  | MLcons(_,GlobRef.ConstructRef ((kn,0),1),l) ->
     MutInd.equal kn ind_ascii && check_extract_ascii () && is_list_cons l
   | _ -> false
 
 let get_native_char c =
   let rec cumul = function
     | [] -> 0
-    | MLcons(_,ConstructRef(_,j),[])::l -> (2-j) + 2 * (cumul l)
+    | MLcons(_,GlobRef.ConstructRef(_,j),[])::l -> (2-j) + 2 * (cumul l)
     | _ -> assert false
   in
   let l = match c with MLcons(_,_,l) -> l | _ -> assert false in
diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml
index ca1520594d..551dbdc6fb 100644
--- a/plugins/extraction/extract_env.ml
+++ b/plugins/extraction/extract_env.ml
@@ -14,7 +14,6 @@ open Declarations
 open Names
 open ModPath
 open Libnames
-open Globnames
 open Pp
 open CErrors
 open Util
@@ -118,7 +117,7 @@ module Visit : VISIT = struct
     v.mp <- MPset.union (prefixes_mp mp) v.mp;
     v.mp_all <- MPset.add mp v.mp_all
   let add_kn kn = v.kn <- KNset.add kn v.kn; add_mp (KerName.modpath kn)
-  let add_ref = function
+  let add_ref = let open GlobRef in function
     | ConstRef c -> add_kn (Constant.user c)
     | IndRef (ind,_) | ConstructRef ((ind,_),_) -> add_kn (MutInd.user ind)
     | VarRef _ -> assert false
@@ -761,7 +760,7 @@ let show_extraction ~pstate =
     let ast, ty = extract_constr env sigma t in
     let mp = Lib.current_mp () in
     let l = Label.of_id (Proof_global.get_proof_name pstate) in
-    let fake_ref = ConstRef (Constant.make2 mp l) in
+    let fake_ref = GlobRef.ConstRef (Constant.make2 mp l) in
     let decl = Dterm (fake_ref, ast, ty) in
     print_one_decl [] mp decl
   in
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index d0ad21a13e..78c6255c1e 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -24,7 +24,6 @@ open Termops
 open Inductiveops
 open Recordops
 open Namegen
-open Globnames
 open Miniml
 open Table
 open Mlutil
@@ -303,7 +302,7 @@ let rec extract_type env sg db j c args =
 	       else let n' = List.nth db (n-1) in
 	       if Int.equal n' 0 then Tunknown else Tvar n')
     | Const (kn,u) ->
-        let r = ConstRef kn in
+        let r = GlobRef.ConstRef kn in
         let typ = type_of env sg (EConstr.mkConstU (kn,u)) in
         (match flag_of_type env sg typ with
 	   | (Logic,_) -> assert false (* Cf. logical cases above *)
@@ -311,7 +310,7 @@ let rec extract_type env sg db j c args =
                let mlt = extract_type_app env sg db (r, type_sign env sg typ) args in
                (match (lookup_constant kn env).const_body with
                  | Undef _ | OpaqueDef _ | Primitive _ -> mlt
-                 | Def _ when is_custom (ConstRef kn) -> mlt
+                 | Def _ when is_custom (GlobRef.ConstRef kn) -> mlt
                  | Def lbody ->
                       let newc = applistc (get_body lbody) args in
                       let mlt' = extract_type env sg db j newc [] in
@@ -331,7 +330,7 @@ let rec extract_type env sg db j c args =
                       extract_type env sg db j newc []))
     | Ind ((kn,i),u) ->
         let s = (extract_ind env kn).ind_packets.(i).ip_sign in
-        extract_type_app env sg db (IndRef (kn,i),s) args
+        extract_type_app env sg db (GlobRef.IndRef (kn,i),s) args
     | Proj (p,t) ->
        (* Let's try to reduce, if it hasn't already been done. *)
        if Projection.unfolded p then Tunknown
@@ -346,7 +345,7 @@ let rec extract_type env sg db j c args =
         | LocalDef (_,body,_) ->
            extract_type env sg db j (EConstr.applist (body,args)) []
         | LocalAssum (_,ty) ->
-           let r = VarRef v in
+           let r = GlobRef.VarRef v in
            (match flag_of_type env sg ty with
             | (Logic,_) -> assert false (* Cf. logical cases above *)
             | (Info, TypeScheme) ->
@@ -405,7 +404,7 @@ and extract_ind env kn = (* kn is supposed to be in long form *)
        extract_really_ind env kn mib
      with SingletonInductiveBecomesProp id ->
        (* TODO : which inductive is concerned in the block ? *)
-       error_singleton_become_prop id (Some (IndRef (kn,0)))
+       error_singleton_become_prop id (Some (GlobRef.IndRef (kn,0)))
 
 (* Then the real function *)
 
@@ -481,7 +480,7 @@ and extract_really_ind env kn mib =
     let ind_info =
       try
 	let ip = (kn, 0) in
-	let r = IndRef ip in
+        let r = GlobRef.IndRef ip in
 	if is_custom r then raise (I Standard);
         if mib.mind_finite == CoFinite then raise (I Coinductive);
 	if not (Int.equal mib.mind_ntypes 1) then raise (I Standard);
@@ -519,7 +518,7 @@ and extract_really_ind env kn mib =
 	      (* Is it safe to use [id] for projections [foo.id] ? *)
 	      if List.for_all ((==) Keep) (type2signature env typ)
 	      then projs := Cset.add knp !projs;
-	      Some (ConstRef knp) :: (select_fields l typs)
+              Some (GlobRef.ConstRef knp) :: (select_fields l typs)
 	  | _ -> assert false
 	in
 	let field_glob = select_fields field_names typ
@@ -565,7 +564,7 @@ and extract_type_cons env sg db dbmap c i =
 
 (*s Recording the ML type abbreviation of a Coq type scheme constant. *)
 
-and mlt_env env r = match r with
+and mlt_env env r = let open GlobRef in match r with
   | IndRef _ | ConstructRef _ | VarRef _ -> None
   | ConstRef kn ->
      let cb = Environ.lookup_constant kn env in
@@ -688,7 +687,7 @@ let rec extract_term env sg mle mlt c args =
          | LocalDef (_,_,ty) -> ty
        in
        let vty = extract_type env sg [] 0 ty [] in
-       let extract_var mlt = put_magic (mlt,vty) (MLglob (VarRef v)) in
+       let extract_var mlt = put_magic (mlt,vty) (MLglob (GlobRef.VarRef v)) in
        extract_app env sg mle mlt extract_var args
     | Int i -> assert (args = []); MLuint i
     | Ind _ | Prod _ | Sort _ -> assert false
@@ -746,10 +745,10 @@ and extract_cst_app env sg mle mlt kn args =
   (* Second, is the resulting type compatible with the expected type [mlt] ? *)
   let magic2 = needs_magic (a, mlt) in
   (* The internal head receives a magic if [magic1] *)
-  let head = put_magic_if magic1 (MLglob (ConstRef kn)) in
+  let head = put_magic_if magic1 (MLglob (GlobRef.ConstRef kn)) in
   (* Now, the extraction of the arguments. *)
   let s_full = type2signature env (snd schema) in
-  let s_full = sign_with_implicits (ConstRef kn) s_full 0 in
+  let s_full = sign_with_implicits (GlobRef.ConstRef kn) s_full 0 in
   let s = sign_no_final_keeps s_full in
   let ls = List.length s in
   let la = List.length args in
@@ -762,7 +761,7 @@ and extract_cst_app env sg mle mlt kn args =
         (* for better optimisations later, we discard dependent args
            of projections and replace them by fake args that will be
            removed during final pretty-print. *)
-	let l,l' = List.chop (projection_arity (ConstRef kn)) mla in
+        let l,l' = List.chop (projection_arity (GlobRef.ConstRef kn)) mla in
 	if not (List.is_empty l') then (List.map (fun _ -> MLexn "Proj Args") l) @ l'
 	else mla
       with e when CErrors.noncritical e -> mla
@@ -807,11 +806,11 @@ and extract_cons_app env sg mle mlt (((kn,i) as ip,j) as cp) args =
   let nb_tvars = List.length oi.ip_vars
   and types = List.map (expand env) oi.ip_types.(j-1) in
   let list_tvar = List.map (fun i -> Tvar i) (List.interval 1 nb_tvars) in
-  let type_cons = type_recomp (types, Tglob (IndRef ip, list_tvar)) in
+  let type_cons = type_recomp (types, Tglob (GlobRef.IndRef ip, list_tvar)) in
   let type_cons = instantiation (nb_tvars, type_cons) in
   (* Then, the usual variables [s], [ls], [la], ... *)
   let s = List.map (type2sign env) types in
-  let s = sign_with_implicits (ConstructRef cp) s params_nb in
+  let s = sign_with_implicits (GlobRef.ConstructRef cp) s params_nb in
   let ls = List.length s in
   let la = List.length args in
   assert (la <= ls + params_nb);
@@ -831,8 +830,8 @@ and extract_cons_app env sg mle mlt (((kn,i) as ip,j) as cp) args =
 	| Tglob (_,l) -> List.map type_simpl l
 	| _ -> assert false
       in
-      let typ = Tglob(IndRef ip, typeargs) in
-      put_magic_if magic1 (MLcons (typ, ConstructRef cp, mla))
+      let typ = Tglob(GlobRef.IndRef ip, typeargs) in
+      put_magic_if magic1 (MLcons (typ, GlobRef.ConstructRef cp, mla))
   in
   (* Different situations depending of the number of arguments: *)
   if la < params_nb then
@@ -880,11 +879,11 @@ and extract_case env sg mle ((kn,i) as ip,c,br) mlt =
       let oi = mi.ind_packets.(i) in
       let metas = Array.init (List.length oi.ip_vars) new_meta in
       (* The extraction of the head. *)
-      let type_head = Tglob (IndRef ip, Array.to_list metas) in
+      let type_head = Tglob (GlobRef.IndRef ip, Array.to_list metas) in
       let a = extract_term env sg mle type_head c [] in
       (* The extraction of each branch. *)
       let extract_branch i =
-	let r = ConstructRef (ip,i+1) in
+        let r = GlobRef.ConstructRef (ip,i+1) in
 	(* The types of the arguments of the corresponding constructor. *)
 	let f t = type_subst_vect metas (expand env t) in
 	let l = List.map f oi.ip_types.(i) in
@@ -909,7 +908,7 @@ and extract_case env sg mle ((kn,i) as ip,c,br) mlt =
       else
 	(* Standard case: we apply [extract_branch]. *)
 	let typs = List.map type_simpl (Array.to_list metas) in
-	let typ = Tglob (IndRef ip,typs) in
+        let typ = Tglob (GlobRef.IndRef ip,typs) in
 	MLcase (typ, a, Array.init br_size extract_branch)
 
 (*s Extraction of a (co)-fixpoint. *)
@@ -960,7 +959,7 @@ let extract_std_constant env sg kn body typ =
   let l,t' = type_decomp (expand env (var2var' t)) in
   let s = List.map (type2sign env) l in
   (* Check for user-declared implicit information *)
-  let s = sign_with_implicits (ConstRef kn) s 0 in
+  let s = sign_with_implicits (GlobRef.ConstRef kn) s 0 in
   (* Decomposing the top level lambdas of [body].
      If there isn't enough, it's ok, as long as remaining args
      aren't to be pruned (and initial lambdas aren't to be all
@@ -1015,7 +1014,7 @@ let extract_axiom env sg kn typ =
   let l,_ = type_decomp (expand env (var2var' t)) in
   let s = List.map (type2sign env) l in
   (* Check for user-declared implicit information *)
-  let s = sign_with_implicits (ConstRef kn) s 0 in
+  let s = sign_with_implicits (GlobRef.ConstRef kn) s 0 in
   type_expunge_from_sign env s t
 
 let extract_fixpoint env sg vkn (fi,ti,ci) =
@@ -1034,10 +1033,10 @@ let extract_fixpoint env sg vkn (fi,ti,ci) =
         terms.(i) <- e;
         types.(i) <- t;
       with SingletonInductiveBecomesProp id ->
-        error_singleton_become_prop id (Some (ConstRef vkn.(i)))
+        error_singleton_become_prop id (Some (GlobRef.ConstRef vkn.(i)))
   done;
   current_fixpoints := [];
-  Dfix (Array.map (fun kn -> ConstRef kn) vkn, terms, types)
+  Dfix (Array.map (fun kn -> GlobRef.ConstRef kn) vkn, terms, types)
 
 (** Because of automatic unboxing the easy way [mk_def c] on the
    constant body of primitive projections doesn't work. We pretend
@@ -1095,7 +1094,7 @@ let fake_match_projection env p =
 
 let extract_constant env kn cb =
   let sg = Evd.from_env env in
-  let r = ConstRef kn in
+  let r = GlobRef.ConstRef kn in
   let typ = EConstr.of_constr cb.const_type in
   let warn_info () = if not (is_custom r) then add_info_axiom r in
   let warn_log () = if not (constant_has_body cb) then add_log_axiom r
@@ -1150,11 +1149,11 @@ let extract_constant env kn cb =
             if access_opaque () then mk_def (get_opaque env c)
             else mk_ax ())
   with SingletonInductiveBecomesProp id ->
-    error_singleton_become_prop id (Some (ConstRef kn))
+    error_singleton_become_prop id (Some (GlobRef.ConstRef kn))
 
 let extract_constant_spec env kn cb =
   let sg = Evd.from_env env in
-  let r = ConstRef kn in
+  let r = GlobRef.ConstRef kn in
   let typ = EConstr.of_constr cb.const_type in
   try
     match flag_of_type env sg typ with
@@ -1173,7 +1172,7 @@ let extract_constant_spec env kn cb =
         let t = snd (record_constant_type env sg kn (Some typ)) in
         Sval (r, type_expunge env t)
   with SingletonInductiveBecomesProp id ->
-    error_singleton_become_prop id (Some (ConstRef kn))
+    error_singleton_become_prop id (Some (GlobRef.ConstRef kn))
 
 let extract_with_type env sg c =
   try
@@ -1205,7 +1204,7 @@ let extract_inductive env kn =
   let ind = extract_ind env kn in
   add_recursors env kn;
   let f i j l =
-    let implicits = implicits_of_global (ConstructRef ((kn,i),j+1)) in
+    let implicits = implicits_of_global (GlobRef.ConstructRef ((kn,i),j+1)) in
     let rec filter i = function
       | [] -> []
       | t::l ->
diff --git a/plugins/extraction/haskell.ml b/plugins/extraction/haskell.ml
index a62fb1a728..e4efbcff0c 100644
--- a/plugins/extraction/haskell.ml
+++ b/plugins/extraction/haskell.ml
@@ -14,7 +14,6 @@ open Pp
 open CErrors
 open Util
 open Names
-open Globnames
 open Table
 open Miniml
 open Mlutil
@@ -110,7 +109,7 @@ let rec pp_type par vl t =
       (try Id.print (List.nth vl (pred i))
        with Failure _ -> (str "a" ++ int i))
     | Tglob (r,[]) -> pp_global Type r
-    | Tglob (IndRef(kn,0),l)
+    | Tglob (GlobRef.IndRef(kn,0),l)
 	when not (keep_singleton ()) && MutInd.equal kn (mk_ind "Coq.Init.Specif" "sig") ->
 	  pp_type true vl (List.hd l)
     | Tglob (r,l) ->
@@ -271,7 +270,7 @@ let pp_logical_ind packet =
 	      prvect_with_sep spc Id.print packet.ip_consnames)
 
 let pp_singleton kn packet =
-  let name = pp_global Type (IndRef (kn,0)) in
+  let name = pp_global Type (GlobRef.IndRef (kn,0)) in
   let l = rename_tvars keywords packet.ip_vars in
   hov 2 (str "type " ++ name ++ spc () ++
 	 prlist_with_sep spc Id.print l ++
@@ -291,14 +290,14 @@ let pp_one_ind ip pl cv =
 		  (fun () -> (str " ")) (pp_type true pl) l))
   in
   str (if Array.is_empty cv then "type " else "data ") ++
-  pp_global Type (IndRef ip) ++
+  pp_global Type (GlobRef.IndRef ip) ++
   prlist_strict (fun id -> str " " ++ pr_lower_id id) pl ++ str " =" ++
   if Array.is_empty cv then str " () -- empty inductive"
   else
     (fnl () ++ str " " ++
      v 0 (str "  " ++
 	  prvect_with_sep (fun () -> fnl () ++ str "| ") pp_constructor
-	    (Array.mapi (fun i c -> ConstructRef (ip,i+1),c) cv)))
+            (Array.mapi (fun i c -> GlobRef.ConstructRef (ip,i+1),c) cv)))
 
 let rec pp_ind first kn i ind =
   if i >= Array.length ind.ind_packets then
@@ -306,7 +305,7 @@ let rec pp_ind first kn i ind =
   else
     let ip = (kn,i) in
     let p = ind.ind_packets.(i) in
-    if is_custom (IndRef (kn,i)) then pp_ind first kn (i+1) ind
+    if is_custom (GlobRef.IndRef (kn,i)) then pp_ind first kn (i+1) ind
     else
       if p.ip_logical then
 	pp_logical_ind p ++ pp_ind first kn (i+1) ind
diff --git a/plugins/extraction/json.ml b/plugins/extraction/json.ml
index f88d29e9ed..fba6b7c780 100644
--- a/plugins/extraction/json.ml
+++ b/plugins/extraction/json.ml
@@ -1,7 +1,6 @@
 open Pp
 open Util
 open Names
-open Globnames
 open Table
 open Miniml
 open Mlutil
@@ -200,10 +199,10 @@ and json_function env t =
 
 let json_ind ip pl cv = json_dict [
     ("what", json_str "decl:ind");
-    ("name", json_global Type (IndRef ip));
+    ("name", json_global Type (GlobRef.IndRef ip));
     ("argnames", json_list (List.map json_id pl));
     ("constructors", json_listarr (Array.mapi (fun idx c -> json_dict [
-        ("name", json_global Cons (ConstructRef (ip, idx+1)));
+        ("name", json_global Cons (GlobRef.ConstructRef (ip, idx+1)));
         ("argtypes", json_list (List.map (json_type pl) c))
       ]) cv))
   ]
diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml
index a8d766cd6e..2d5872718f 100644
--- a/plugins/extraction/mlutil.ml
+++ b/plugins/extraction/mlutil.ml
@@ -12,7 +12,6 @@
 open Util
 open Names
 open Libnames
-open Globnames
 open Table
 open Miniml
 (*i*)
@@ -668,11 +667,11 @@ let is_regular_match br =
 	  | _ -> raise Impossible
       in
       let ind = match get_r br.(0) with
-	| ConstructRef (ind,_) -> ind
+        | GlobRef.ConstructRef (ind,_) -> ind
 	| _ -> raise Impossible
       in
       let is_ref i tr = match get_r tr with
-      | ConstructRef (ind', j) -> eq_ind ind ind' && Int.equal j (i + 1)
+      | GlobRef.ConstructRef (ind', j) -> eq_ind ind ind' && Int.equal j (i + 1)
       | _ -> false
       in
       Array.for_all_i is_ref 0 br
@@ -819,11 +818,11 @@ let rec tmp_head_lams = function
 *)
 
 let rec ast_glob_subst s t = match t with
-  | MLapp ((MLglob ((ConstRef kn) as refe)) as f, a) ->
+  | MLapp ((MLglob ((GlobRef.ConstRef kn) as refe)) as f, a) ->
       let a = List.map (fun e -> tmp_head_lams (ast_glob_subst s e)) a in
       (try linear_beta_red a (Refmap'.find refe s)
        with Not_found -> MLapp (f, a))
-  | MLglob ((ConstRef kn) as refe) ->
+  | MLglob ((GlobRef.ConstRef kn) as refe) ->
       (try Refmap'.find refe s with Not_found -> t)
   | _ -> ast_map (ast_glob_subst s) t
 
@@ -1504,7 +1503,7 @@ open Declareops
 let inline_test r t =
   if not (auto_inline ()) then false
   else
-    let c = match r with ConstRef c -> c | _ -> assert false in
+    let c = match r with GlobRef.ConstRef c -> c | _ -> assert false in
     let has_body =
       try constant_has_body (Global.lookup_constant c)
       with Not_found -> false
@@ -1534,7 +1533,7 @@ let manual_inline_set =
     Cset_env.empty
 
 let manual_inline = function
-  | ConstRef c -> Cset_env.mem c manual_inline_set
+  | GlobRef.ConstRef c -> Cset_env.mem c manual_inline_set
   | _ -> false
 
 (* If the user doesn't say he wants to keep [t], we inline in two cases:
diff --git a/plugins/extraction/modutil.ml b/plugins/extraction/modutil.ml
index bded698ea7..6b1eef7abb 100644
--- a/plugins/extraction/modutil.ml
+++ b/plugins/extraction/modutil.ml
@@ -10,7 +10,6 @@
 
 open Names
 open ModPath
-open Globnames
 open CErrors
 open Util
 open Miniml
@@ -42,7 +41,7 @@ let se_iter do_decl do_spec do_mp =
 	let mp_w =
 	  List.fold_left (fun mp l -> MPdot(mp,Label.of_id l)) mp_mt idl'
 	in
-	let r = ConstRef (Constant.make2 mp_w (Label.of_id l')) in
+        let r = GlobRef.ConstRef (Constant.make2 mp_w (Label.of_id l')) in
         mt_iter mt; do_spec (Stype(r,l,Some t))
     | MTwith (mt,ML_With_module(idl,mp))->
         let mp_mt = msid_of_mt mt in
@@ -113,12 +112,12 @@ let ast_iter_references do_term do_cons do_type a =
 
 let ind_iter_references do_term do_cons do_type kn ind =
   let type_iter = type_iter_references do_type in
-  let cons_iter cp l = do_cons (ConstructRef cp); List.iter type_iter l in
+  let cons_iter cp l = do_cons (GlobRef.ConstructRef cp); List.iter type_iter l in
   let packet_iter ip p =
-    do_type (IndRef ip);
+    do_type (GlobRef.IndRef ip);
     if lang () == Ocaml then
       (match ind.ind_equiv with
-	 | Miniml.Equiv kne -> do_type (IndRef (MutInd.make1 kne, snd ip));
+         | Miniml.Equiv kne -> do_type (GlobRef.IndRef (MutInd.make1 kne, snd ip));
 	 | _ -> ());
     Array.iteri (fun j -> cons_iter (ip,j+1)) p.ip_types
   in
@@ -258,7 +257,7 @@ let dfix_to_mlfix rv av i =
   let s = make_subst (Array.length rv - 1) Refmap'.empty
   in
   let rec subst n t = match t with
-    | MLglob ((ConstRef kn) as refe) ->
+    | MLglob ((GlobRef.ConstRef kn) as refe) ->
 	(try MLrel (n + (Refmap'.find refe s)) with Not_found -> t)
     | _ -> ast_map_lift subst n t
   in
@@ -309,7 +308,7 @@ and optim_me to_appear s = function
    For non-library extraction, we recompute a minimal set of dependencies
    for first-level definitions (no module pruning yet). *)
 
-let base_r = function
+let base_r = let open GlobRef in function
   | ConstRef c as r -> r
   | IndRef (kn,_) -> IndRef (kn,0)
   | ConstructRef ((kn,_),_) -> IndRef (kn,0)
@@ -327,7 +326,7 @@ let reset_needed, add_needed, add_needed_mp, found_needed, is_needed =
      Refset'.mem r !needed || MPset.mem (modpath_of_r r) !needed_mps))
 
 let declared_refs = function
-  | Dind (kn,_) -> [IndRef (kn,0)]
+  | Dind (kn,_) -> [GlobRef.IndRef (kn,0)]
   | Dtype (r,_,_) -> [r]
   | Dterm (r,_,_) -> [r]
   | Dfix (rv,_,_) -> Array.to_list rv
diff --git a/plugins/extraction/ocaml.ml b/plugins/extraction/ocaml.ml
index 21a8b8e5fb..75fb35192b 100644
--- a/plugins/extraction/ocaml.ml
+++ b/plugins/extraction/ocaml.ml
@@ -15,7 +15,6 @@ open CErrors
 open Util
 open Names
 open ModPath
-open Globnames
 open Table
 open Miniml
 open Mlutil
@@ -142,7 +141,7 @@ let get_infix r =
   let s = find_custom r in
   String.sub s 1 (String.length s - 2)
 
-let get_ind = function
+let get_ind = let open GlobRef in function
   | IndRef _ as r -> r
   | ConstructRef (ind,_) -> IndRef ind
   | _ -> assert false
@@ -166,7 +165,7 @@ let pp_type par vl t =
     | Tglob (r,[a1;a2]) when is_infix r ->
 	pp_par par (pp_rec true a1 ++ str (get_infix r) ++ pp_rec true a2)
     | Tglob (r,[]) -> pp_global Type r
-    | Tglob (IndRef(kn,0),l)
+    | Tglob (GlobRef.IndRef(kn,0),l)
 	when not (keep_singleton ()) && MutInd.equal kn (mk_ind "Coq.Init.Specif" "sig") ->
 	pp_tuple_light pp_rec l
     | Tglob (r,l) ->
@@ -467,7 +466,7 @@ let pp_Dfix (rv,c,t) =
 let pp_equiv param_list name = function
   | NoEquiv, _ -> mt ()
   | Equiv kn, i ->
-      str " = " ++ pp_parameters param_list ++ pp_global Type (IndRef (MutInd.make1 kn,i))
+      str " = " ++ pp_parameters param_list ++ pp_global Type (GlobRef.IndRef (MutInd.make1 kn,i))
   | RenEquiv ren, _  ->
       str " = " ++ pp_parameters param_list ++ str (ren^".") ++ name
 
@@ -494,7 +493,7 @@ let pp_logical_ind packet =
   fnl ()
 
 let pp_singleton kn packet =
-  let name = pp_global Type (IndRef (kn,0)) in
+  let name = pp_global Type (GlobRef.IndRef (kn,0)) in
   let l = rename_tvars keywords packet.ip_vars in
   hov 2 (str "type " ++ pp_parameters l ++ name ++ str " =" ++ spc () ++
 	 pp_type false l (List.hd packet.ip_types.(0)) ++ fnl () ++
@@ -502,7 +501,7 @@ let pp_singleton kn packet =
 		     Id.print packet.ip_consnames.(0)))
 
 let pp_record kn fields ip_equiv packet =
-  let ind = IndRef (kn,0) in
+  let ind = GlobRef.IndRef (kn,0) in
   let name = pp_global Type ind in
   let fieldnames = pp_fields ind fields in
   let l = List.combine fieldnames packet.ip_types.(0) in
@@ -525,13 +524,13 @@ let pp_ind co kn ind =
   let nextkwd = fnl () ++ str "and " in
   let names =
     Array.mapi (fun i p -> if p.ip_logical then mt () else
-		  pp_global Type (IndRef (kn,i)))
+                  pp_global Type (GlobRef.IndRef (kn,i)))
       ind.ind_packets
   in
   let cnames =
     Array.mapi
       (fun i p -> if p.ip_logical then [||] else
-	 Array.mapi (fun j _ -> pp_global Cons (ConstructRef ((kn,i),j+1)))
+         Array.mapi (fun j _ -> pp_global Cons (GlobRef.ConstructRef ((kn,i),j+1)))
 	   p.ip_types)
       ind.ind_packets
   in
@@ -541,7 +540,7 @@ let pp_ind co kn ind =
       let ip = (kn,i) in
       let ip_equiv = ind.ind_equiv, i in
       let p = ind.ind_packets.(i) in
-      if is_custom (IndRef ip) then pp (i+1) kwd
+      if is_custom (GlobRef.IndRef ip) then pp (i+1) kwd
       else if p.ip_logical then pp_logical_ind p ++ pp (i+1) kwd
       else
 	kwd ++ (if co then pp_coind p.ip_vars names.(i) else mt ()) ++
@@ -672,7 +671,7 @@ and pp_module_type params = function
       let mp_w =
 	List.fold_left (fun mp l -> MPdot(mp,Label.of_id l)) mp_mt idl'
       in
-      let r = ConstRef (Constant.make2 mp_w (Label.of_id l)) in
+      let r = GlobRef.ConstRef (Constant.make2 mp_w (Label.of_id l)) in
       push_visible mp_mt [];
       let pp_w = str " with type " ++ ids ++ pp_global Type r in
       pop_visible();
diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml
index b09a81e1c8..96a3d00dc2 100644
--- a/plugins/extraction/table.ml
+++ b/plugins/extraction/table.ml
@@ -30,12 +30,12 @@ module Refset' = GlobRef.Set_env
 
 (*S Utilities about [module_path] and [kernel_names] and [global_reference] *)
 
-let occur_kn_in_ref kn = function
+let occur_kn_in_ref kn = let open GlobRef in function
   | IndRef (kn',_)
   | ConstructRef ((kn',_),_) -> MutInd.equal kn kn'
   | ConstRef _ | VarRef _ -> false
 
-let repr_of_r = function
+let repr_of_r = let open GlobRef in function
   | ConstRef kn -> Constant.repr2 kn
   | IndRef (kn,_)
   | ConstructRef ((kn,_),_) -> MutInd.repr2 kn
@@ -151,7 +151,7 @@ let init_inductive_kinds () = inductive_kinds := Mindmap_env.empty
 let add_inductive_kind kn k =
     inductive_kinds := Mindmap_env.add kn k !inductive_kinds
 let is_coinductive r =
-  let kn = match r with
+  let kn = let open GlobRef in match r with
     | ConstructRef ((kn,_),_) -> kn
     | IndRef (kn,_) -> kn
     | _ -> assert false
@@ -164,7 +164,7 @@ let is_coinductive_type = function
   | _ -> false
 
 let get_record_fields r =
-  let kn = match r with
+  let kn = let open GlobRef in match r with
     | ConstructRef ((kn,_),_) -> kn
     | IndRef (kn,_) -> kn
     | _ -> assert false
@@ -201,7 +201,7 @@ let add_recursors env ind =
     mib.mind_packets
 
 let is_recursor = function
-  | ConstRef c -> KNset.mem (Constant.canonical c) !recursors
+  | GlobRef.ConstRef c -> KNset.mem (Constant.canonical c) !recursors
   | _ -> false
 
 (*s Record tables. *)
@@ -210,7 +210,7 @@ let is_recursor = function
 
 let projs = ref (GlobRef.Map.empty : (inductive*int) GlobRef.Map.t)
 let init_projs () = projs := GlobRef.Map.empty
-let add_projection n kn ip = projs := GlobRef.Map.add (ConstRef kn) (ip,n) !projs
+let add_projection n kn ip = projs := GlobRef.Map.add (GlobRef.ConstRef kn) (ip,n) !projs
 let is_projection r = GlobRef.Map.mem r !projs
 let projection_arity r = snd (GlobRef.Map.find r !projs)
 let projection_info r = GlobRef.Map.find r !projs
@@ -264,6 +264,7 @@ let safe_basename_of_global r =
     with Not_found ->
       anomaly (Pp.str "Inductive object unknown to extraction and not globally visible.")
   in
+  let open GlobRef in
   match r with
     | ConstRef kn -> Label.to_id (Constant.label kn)
     | IndRef (kn,0) -> Label.to_id (MutInd.label kn)
@@ -286,7 +287,7 @@ let safe_pr_global r = str (string_of_global r)
 let safe_pr_long_global r =
   try Printer.pr_global r
   with Not_found -> match r with
-    | ConstRef kn ->
+    | GlobRef.ConstRef kn ->
         let mp,l = Constant.repr2 kn in
 	str ((ModPath.to_string mp)^"."^(Label.to_string l))
     | _ -> assert false
@@ -658,7 +659,7 @@ let extraction_inline b l =
   let refs = List.map Smartlocate.global_with_alias l in
   List.iter
     (fun r -> match r with
-       | ConstRef _ -> ()
+       | GlobRef.ConstRef _ -> ()
        | _ -> error_constant r) refs;
   Lib.add_anonymous_leaf (inline_extraction (b,refs))
 
@@ -666,7 +667,7 @@ let extraction_inline b l =
 
 let print_extraction_inline () =
   let (i,n)= !inline_table in
-  let i'= Refset'.filter (function ConstRef _ -> true | _ -> false) i in
+  let i'= Refset'.filter (function GlobRef.ConstRef _ -> true | _ -> false) i in
     (str "Extraction Inline:" ++ fnl () ++
      Refset'.fold
        (fun r p ->
@@ -823,8 +824,8 @@ let indref_of_match pv =
   if Array.is_empty pv then raise Not_found;
   let (_,pat,_) = pv.(0) in
   match pat with
-    | Pusual (ConstructRef (ip,_)) -> IndRef ip
-    | Pcons (ConstructRef (ip,_),_) -> IndRef ip
+    | Pusual (GlobRef.ConstructRef (ip,_)) -> GlobRef.IndRef ip
+    | Pcons (GlobRef.ConstructRef (ip,_),_) -> GlobRef.IndRef ip
     | _ -> raise Not_found
 
 let is_custom_match pv =
@@ -852,9 +853,9 @@ let extract_constant_inline inline r ids s =
   check_inside_section ();
   let g = Smartlocate.global_with_alias r in
   match g with
-    | ConstRef kn ->
+    | GlobRef.ConstRef kn ->
 	let env = Global.env () in
-        let typ, _ = Typeops.type_of_global_in_context env (ConstRef kn) in
+        let typ, _ = Typeops.type_of_global_in_context env (GlobRef.ConstRef kn) in
 	let typ = Reduction.whd_all env typ in
 	if Reduction.is_arity env typ
 	  then begin
@@ -871,7 +872,7 @@ let extract_inductive r s l optstr =
   let g = Smartlocate.global_with_alias r in
   Dumpglob.add_glob ?loc:r.CAst.loc g;
   match g with
-    | IndRef ((kn,i) as ip) ->
+    | GlobRef.IndRef ((kn,i) as ip) ->
 	let mib = Global.lookup_mind kn in
 	let n = Array.length mib.mind_packets.(i).mind_consnames in
 	if not (Int.equal n (List.length l)) then error_nb_cons ();
@@ -881,7 +882,7 @@ let extract_inductive r s l optstr =
 	  optstr;
 	List.iteri
 	  (fun j s ->
-	     let g = ConstructRef (ip,succ j) in
+             let g = GlobRef.ConstructRef (ip,succ j) in
 	     Lib.add_anonymous_leaf (inline_extraction (true,[g]));
 	     Lib.add_anonymous_leaf (in_customs (g,[],s))) l
     | _ -> error_inductive g