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

33 files changed, 154 insertions, 178 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
diff --git a/plugins/firstorder/formula.ml b/plugins/firstorder/formula.ml
index 2d5ea9536c..fb363b9393 100644
--- a/plugins/firstorder/formula.ml
+++ b/plugins/firstorder/formula.ml
@@ -15,7 +15,6 @@ open EConstr
 open Vars
 open Util
 open Declarations
-open Globnames
 
 module RelDecl = Context.Rel.Declaration
 
@@ -124,7 +123,7 @@ type side = Hyp | Concl | Hint
 
 let no_atoms = (false,{positive=[];negative=[]})
 
-let dummy_id=VarRef (Id.of_string "_") (* "_" cannot be parsed *)
+let dummy_id=GlobRef.VarRef (Id.of_string "_") (* "_" cannot be parsed *)
 
 let build_atoms env sigma metagen side cciterm =
   let trivial =ref false
diff --git a/plugins/firstorder/ground.ml b/plugins/firstorder/ground.ml
index bdf339a488..e134562702 100644
--- a/plugins/firstorder/ground.ml
+++ b/plugins/firstorder/ground.ml
@@ -15,12 +15,11 @@ open Rules
 open Instances
 open Tacmach.New
 open Tacticals.New
-open Globnames
 
 let update_flags ()=
   let open TransparentState in
   let f accu coe = match coe.Classops.coe_value with
-    | ConstRef kn -> { accu with tr_cst = Names.Cpred.remove kn accu.tr_cst }
+    | Names.GlobRef.ConstRef kn -> { accu with tr_cst = Names.Cpred.remove kn accu.tr_cst }
     | _ -> accu
   in
   let flags = List.fold_left f TransparentState.full (Classops.coercions ()) in
diff --git a/plugins/firstorder/rules.ml b/plugins/firstorder/rules.ml
index f3a16cd13e..79386f7ac9 100644
--- a/plugins/firstorder/rules.ml
+++ b/plugins/firstorder/rules.ml
@@ -20,7 +20,6 @@ open Proofview.Notations
 open Termops
 open Formula
 open Sequent
-open Globnames
 
 module NamedDecl = Context.Named.Declaration
 
@@ -48,7 +47,7 @@ let wrap n b continue seq =
 	      List.exists (occur_var_in_decl env sigma id) ctx then
 		(aux (i-1) q (nd::ctx))
 	    else
-	      add_formula env sigma Hyp (VarRef id) (NamedDecl.get_type nd) (aux (i-1) q (nd::ctx)) in
+              add_formula env sigma Hyp (GlobRef.VarRef id) (NamedDecl.get_type nd) (aux (i-1) q (nd::ctx)) in
   let seq1=aux n nc [] in
   let seq2=if b then
     add_formula env sigma Concl dummy_id (pf_concl gls) seq1 else seq1 in
@@ -56,7 +55,7 @@ let wrap n b continue seq =
   end
 
 let clear_global=function
-    VarRef id-> clear [id]
+  | GlobRef.VarRef id-> clear [id]
   | _->tclIDTAC
 
 (* connection rules *)
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 0efb27e3f0..08298bf02c 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -14,7 +14,6 @@ open Tacticals
 open Tactics
 open Indfun_common
 open Libnames
-open Globnames
 open Context.Rel.Declaration
 
 module RelDecl = Context.Rel.Declaration
@@ -1027,7 +1026,7 @@ let do_replace (evd:Evd.evar_map ref) params rec_arg_num rev_args_id f fun_num a
               update_Function
                 {finfos with
                    equation_lemma = Some (match Nametab.locate (qualid_of_ident equation_lemma_id) with
-                                              ConstRef c -> c
+                                              GlobRef.ConstRef c -> c
                                             | _ -> CErrors.anomaly (Pp.str "Not a constant.")
                                          )
                 }
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index cb7a509829..d34faa22fa 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -84,7 +84,7 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type =
   let env_with_params_and_predicates = List.fold_right Environ.push_named new_predicates env_with_params in
   let rel_as_kn =
     fst (match princ_type_info.indref with
-           | Some (Globnames.IndRef ind) -> ind
+           | Some (GlobRef.IndRef ind) -> ind
            | _ -> user_err Pp.(str "Not a valid predicate")
         )
   in
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index bcad6cedf1..6dc01a9f8f 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -6,7 +6,6 @@ open Context
 open Vars
 open Glob_term
 open Glob_ops
-open Globnames
 open Indfun_common
 open CErrors
 open Util
@@ -312,7 +311,7 @@ let build_constructors_of_type ind' argl =
   let npar = mib.Declarations.mind_nparams in
   Array.mapi (fun i _ ->
 		let construct = ind',i+1 in
-		let constructref = ConstructRef(construct) in
+                let constructref = GlobRef.ConstructRef(construct) in
 		let _implicit_positions_of_cst =
 		  Impargs.implicits_of_global constructref
 		in
@@ -328,7 +327,7 @@ let build_constructors_of_type ind' argl =
                     List.make npar (mkGHole ()) @ argl
 		in
 		let pat_as_term =
-		  mkGApp(mkGRef (ConstructRef(ind',i+1)),argl)
+                  mkGApp(mkGRef (GlobRef.ConstructRef(ind',i+1)),argl)
 		in
                 cases_pattern_of_glob_constr (Global.env()) Anonymous pat_as_term
 	     )
@@ -438,7 +437,7 @@ let rec pattern_to_term_and_type env typ  = DAst.with_val (function
       let patl_as_term =
 	List.map2 (pattern_to_term_and_type env)  (List.rev cs_args_types)  patternl
       in
-      mkGApp(mkGRef(ConstructRef constr),
+      mkGApp(mkGRef(GlobRef.ConstructRef constr),
 	     implicit_args@patl_as_term
 	    )
   )
@@ -992,7 +991,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
 		    in
 		    mkGProd(n,t,new_b),id_to_exclude
 		  with Continue ->
-		    let jmeq = Globnames.IndRef (fst (EConstr.destInd Evd.empty (jmeq ()))) in
+                    let jmeq = GlobRef.IndRef (fst (EConstr.destInd Evd.empty (jmeq ()))) in
 		    let ty',ctx = Pretyping.understand env (Evd.from_env env) ty in
                     let ind,args' = Inductiveops.find_inductive env Evd.(from_env env) ty' in
 		    let mib,_ = Global.lookup_inductive (fst ind) in
@@ -1001,7 +1000,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
 		      ((Util.List.chop nparam args'))
 		    in
 		    let rt_typ = DAst.make @@
-		       GApp(DAst.make @@ GRef (Globnames.IndRef (fst ind),None),
+                       GApp(DAst.make @@ GRef (GlobRef.IndRef (fst ind),None),
 			    (List.map
 			      (fun p -> Detyping.detype Detyping.Now false Id.Set.empty
 				 env (Evd.from_env env)
diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml
index 7b758da8e8..d36d86a65b 100644
--- a/plugins/funind/glob_termops.ml
+++ b/plugins/funind/glob_termops.ml
@@ -375,7 +375,7 @@ let rec pattern_to_term pt = DAst.with_val (function
       let patl_as_term =
 	List.map pattern_to_term patternl
       in
-      mkGApp(mkGRef(Globnames.ConstructRef constr),
+      mkGApp(mkGRef(GlobRef.ConstructRef constr),
 	     implicit_args@patl_as_term
 	    )
   ) pt
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index 48e3129599..99efe3e5e2 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -8,7 +8,6 @@ open EConstr
 open Pp
 open Indfun_common
 open Libnames
-open Globnames
 open Glob_term
 open Declarations
 open Tactypes
@@ -59,7 +58,7 @@ let functional_induction with_clean c princl pat =
               let princ,g' =  (* then we get the principle *)
                 try
                   let g',princ =
-                    Tacmach.pf_eapply (Evd.fresh_global) g  (Globnames.ConstRef (Option.get princ_option )) in
+                    Tacmach.pf_eapply (Evd.fresh_global) g  (GlobRef.ConstRef (Option.get princ_option )) in
                   princ,g'
                 with Option.IsNone ->
                   (*i If there is not default lemma defined then,
@@ -836,7 +835,7 @@ let make_graph (f_ref : GlobRef.t) =
   let sigma = Evd.from_env env in
   let c,c_body =
     match f_ref with
-    | ConstRef c ->
+    | GlobRef.ConstRef c ->
       begin try c,Global.lookup_constant c
         with Not_found ->
           raise (UserError (None,str "Cannot find " ++ Printer.pr_leconstr_env env sigma (mkConst c)) )
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index c906670dc0..a119586f7b 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -2,7 +2,6 @@ open Names
 open Pp
 open Constr
 open Libnames
-open Globnames
 open Refiner
 
 let mk_prefix pre id = Id.of_string (pre^(Id.to_string id))
@@ -31,12 +30,12 @@ let locate qid = Nametab.locate qid
 
 let locate_ind ref =
   match locate ref with
-    | IndRef x -> x
+    | GlobRef.IndRef x -> x
     | _ -> raise Not_found
 
 let locate_constant ref =
   match locate ref with
-    | ConstRef x -> x
+    | GlobRef.ConstRef x -> x
     | _ -> raise Not_found
 
 
@@ -129,10 +128,10 @@ let save name const ?hook uctx scope kind =
     | Discharge ->
       let c = SectionLocalDef const in
       let () = declare_variable ~name ~kind c in
-      VarRef name
+      GlobRef.VarRef name
     | Global local ->
       let kn = declare_constant ~name ~kind ~local (DefinitionEntry const) in
-      ConstRef kn
+      GlobRef.ConstRef kn
   in
   DeclareDef.Hook.(call ?hook ~fix_exn { S.uctx; obls = []; scope; dref = r });
   definition_message name
@@ -275,7 +274,7 @@ let pr_info env sigma f_info =
   str "function_constant_type := " ++
   (try
      Printer.pr_lconstr_env env sigma
-       (fst (Typeops.type_of_global_in_context env (ConstRef f_info.function_constant)))
+       (fst (Typeops.type_of_global_in_context env (GlobRef.ConstRef f_info.function_constant)))
    with e when CErrors.noncritical e -> mt ()) ++ fnl () ++
   str "equation_lemma := " ++ pr_ocst env sigma f_info.equation_lemma ++ fnl () ++
   str "completeness_lemma :=" ++ pr_ocst env sigma f_info.completeness_lemma ++ fnl () ++
@@ -299,7 +298,7 @@ let in_Function : function_info -> Libobject.obj =
 
 let find_or_none id =
   try Some
-    (match Nametab.locate (qualid_of_ident id) with ConstRef c -> c | _ -> CErrors.anomaly (Pp.str "Not a constant.")
+    (match Nametab.locate (qualid_of_ident id) with GlobRef.ConstRef c -> c | _ -> CErrors.anomaly (Pp.str "Not a constant.")
     )
   with Not_found -> None
 
@@ -328,7 +327,7 @@ let add_Function is_general f =
   and sprop_lemma = find_or_none (Nameops.add_suffix f_id "_sind")
   and graph_ind =
     match Nametab.locate (qualid_of_ident (mk_rel_id f_id))
-    with | IndRef ind -> ind | _ -> CErrors.anomaly (Pp.str "Not an inductive.")
+    with | GlobRef.IndRef ind -> ind | _ -> CErrors.anomaly (Pp.str "Not an inductive.")
   in
   let finfos =
     { function_constant = f;
@@ -433,8 +432,8 @@ let ltof_ref = function  () -> (find_reference ["Coq";"Arith";"Wf_nat"] "ltof")
 
 let evaluable_of_global_reference r = (* Tacred.evaluable_of_global_reference (Global.env ()) *)
   match r with
-      ConstRef sp -> EvalConstRef sp
-    | VarRef id -> EvalVarRef id
+      GlobRef.ConstRef sp -> EvalConstRef sp
+    | GlobRef.VarRef id -> EvalVarRef id
     | _ -> assert false;;
 
 let list_rewrite (rev:bool) (eqs: (EConstr.constr*bool) list) =
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index 8fa001278b..d4cc31c0af 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -19,7 +19,6 @@ open Context
 open EConstr
 open Vars
 open Pp
-open Globnames
 open Tacticals
 open Tactics
 open Indfun_common
@@ -93,7 +92,7 @@ let make_eq () =
 let generate_type evd g_to_f f graph i =
   (*i we deduce the number of arguments of the function and its returned type from the graph i*)
   let evd',graph =
-    Evd.fresh_global  (Global.env ()) !evd  (Globnames.IndRef (fst (destInd !evd graph)))
+    Evd.fresh_global  (Global.env ()) !evd  (GlobRef.IndRef (fst (destInd !evd graph)))
   in
   evd:=evd';
   let sigma, graph_arity = Typing.type_of (Global.env ()) !evd graph in
@@ -165,7 +164,7 @@ let find_induction_principle evd f =
   match infos.rect_lemma with
     | None -> raise Not_found
     | Some rect_lemma ->
-       let evd',rect_lemma = Evd.fresh_global  (Global.env ()) !evd  (Globnames.ConstRef rect_lemma) in
+       let evd',rect_lemma = Evd.fresh_global  (Global.env ()) !evd  (GlobRef.ConstRef rect_lemma) in
        let evd',typ = Typing.type_of ~refresh:true (Global.env ()) evd' rect_lemma in
        evd:=evd';
        rect_lemma,typ
@@ -978,7 +977,7 @@ let error msg = user_err Pp.(str msg)
 let invfun qhyp f  =
   let f =
     match f with
-      | ConstRef f -> f
+      | GlobRef.ConstRef f -> f
       | _ -> raise (CErrors.UserError(None,str "Not a function"))
   in
   try
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index f4edbda04a..2d8f075aba 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -67,7 +67,7 @@ let find_reference sl s =
 
 let declare_fun name kind ?univs value =
   let ce = definition_entry ?univs value (*FIXME *) in
-  ConstRef(declare_constant ~name ~kind (DefinitionEntry ce))
+  GlobRef.ConstRef(declare_constant ~name ~kind (DefinitionEntry ce))
 
 let defined lemma =
   Lemmas.save_lemma_proved ~lemma ~opaque:Proof_global.Transparent ~idopt:None
@@ -95,7 +95,7 @@ let type_of_const sigma t =
 let constant sl s = UnivGen.constr_of_monomorphic_global (find_reference sl s)
 
 let const_of_ref = function
-    ConstRef kn -> kn
+    GlobRef.ConstRef kn -> kn
   | _ -> anomaly (Pp.str "ConstRef expected.")
 
 (* Generic values *)
@@ -1312,7 +1312,7 @@ let open_new_goal ~lemma build_proof sigma using_lemmas ref_ goal_name (gls_type
       let na_ref = qualid_of_ident na in
       let na_global = Smartlocate.global_with_alias na_ref in
       match na_global with
-          ConstRef c -> is_opaque_constant c
+          GlobRef.ConstRef c -> is_opaque_constant c
         | _ -> anomaly ~label:"equation_lemma" (Pp.str "not a constant.")
     in
     let lemma = mkConst (Names.Constant.make1 (Lib.make_kn na)) in
@@ -1455,7 +1455,7 @@ let com_eqn sign uctx nb_arg eq_name functional_ref f_ref terminate_ref equation
     let open CVars in
     let opacity =
       match terminate_ref with
-        | ConstRef c -> is_opaque_constant c
+        | GlobRef.ConstRef c -> is_opaque_constant c
         | _ -> anomaly ~label:"terminate_lemma" (Pp.str "not a constant.")
     in
     let evd = Evd.from_ctx uctx in
diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml
index db8d09b79e..0e38ce575b 100644
--- a/plugins/ltac/pptactic.ml
+++ b/plugins/ltac/pptactic.ml
@@ -194,7 +194,7 @@ let string_of_genarg_arg (ArgumentType arg) =
 
   let pr_evaluable_reference = function
     | EvalVarRef id -> pr_id id
-    | EvalConstRef sp -> pr_global (Globnames.ConstRef sp)
+    | EvalConstRef sp -> pr_global (GlobRef.ConstRef sp)
 
   let pr_quantified_hypothesis = function
     | AnonHyp n -> int n
@@ -385,7 +385,7 @@ let string_of_genarg_arg (ArgumentType arg) =
   let pr_evaluable_reference_env env = function
     | EvalVarRef id -> pr_id id
     | EvalConstRef sp ->
-      Nametab.pr_global_env (Termops.vars_of_env env) (Globnames.ConstRef sp)
+      Nametab.pr_global_env (Termops.vars_of_env env) (GlobRef.ConstRef sp)
 
   let pr_as_disjunctive_ipat prc ipatl =
     keyword "as" ++ spc () ++
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index 13844c2707..726752a2bf 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -24,7 +24,6 @@ open Tactics
 open Pretype_errors
 open Typeclasses
 open Constrexpr
-open Globnames
 open Evd
 open Tactypes
 open Locus
@@ -1983,8 +1982,8 @@ let add_morphism_as_parameter atts m n : unit =
       (Declare.ParameterEntry (None,(instance,uctx),None))
   in
   Classes.add_instance (Classes.mk_instance
-                  (PropGlobal.proper_class env evd) Hints.empty_hint_info atts.global (ConstRef cst));
-  declare_projection n instance_id (ConstRef cst)
+                  (PropGlobal.proper_class env evd) Hints.empty_hint_info atts.global (GlobRef.ConstRef cst));
+  declare_projection n instance_id (GlobRef.ConstRef cst)
 
 let add_morphism_interactive atts m n : Lemmas.t =
   warn_add_morphism_deprecated ?loc:m.CAst.loc ();
@@ -1997,11 +1996,11 @@ let add_morphism_interactive atts m n : Lemmas.t =
   let kind = Decls.(IsDefinition Instance) in
   let tac = make_tactic "Coq.Classes.SetoidTactics.add_morphism_tactic" in
   let hook { DeclareDef.Hook.S.dref; _ } = dref |> function
-    | Globnames.ConstRef cst ->
+    | GlobRef.ConstRef cst ->
       Classes.add_instance (Classes.mk_instance
                       (PropGlobal.proper_class env evd) Hints.empty_hint_info
-                      atts.global (ConstRef cst));
-      declare_projection n instance_id (ConstRef cst)
+                      atts.global (GlobRef.ConstRef cst));
+      declare_projection n instance_id (GlobRef.ConstRef cst)
     | _ -> assert false
   in
   let hook = DeclareDef.Hook.make hook in
diff --git a/plugins/ltac/taccoerce.ml b/plugins/ltac/taccoerce.ml
index 4e79bab28e..e64129d204 100644
--- a/plugins/ltac/taccoerce.ml
+++ b/plugins/ltac/taccoerce.ml
@@ -203,11 +203,11 @@ let id_of_name = function
         end
        | Const (cst,_) -> Label.to_id (Constant.label cst)
        | Construct (cstr,_) ->
-	  let ref = Globnames.ConstructRef cstr in
+          let ref = GlobRef.ConstructRef cstr in
 	  let basename = Nametab.basename_of_global ref in
 	  basename
        | Ind (ind,_) ->
-	  let ref = Globnames.IndRef ind in
+          let ref = GlobRef.IndRef ind in
 	  let basename = Nametab.basename_of_global ref in
 	  basename
        | Sort s ->
@@ -290,7 +290,7 @@ let coerce_to_evaluable_ref env sigma v =
     if Id.List.mem id (Termops.ids_of_context env) then EvalVarRef id
     else fail ()
   else if has_type v (topwit wit_ref) then
-    let open Globnames in
+    let open GlobRef in
     let r = out_gen (topwit wit_ref) v in
     match r with
     | VarRef var -> EvalVarRef var
diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml
index 3ed5b1aab2..63559cf488 100644
--- a/plugins/ltac/tacintern.ml
+++ b/plugins/ltac/tacintern.ml
@@ -18,7 +18,6 @@ open Tacred
 open Util
 open Names
 open Libnames
-open Globnames
 open Smartlocate
 open Constrexpr
 open Termops
@@ -304,7 +303,7 @@ let intern_evaluable_reference_or_by_notation ist = function
   | {v=ByNotation (ntn,sc);loc} ->
       evaluable_of_global_reference ist.genv
       (Notation.interp_notation_as_global_reference ?loc
-        (function ConstRef _ | VarRef _ -> true | _ -> false) ntn sc)
+        GlobRef.(function ConstRef _ | VarRef _ -> true | _ -> false) ntn sc)
 
 (* Globalize a reduction expression *)
 let intern_evaluable ist r =
@@ -383,7 +382,7 @@ let intern_typed_pattern_or_ref_with_occurrences ist (l,p) =
       | GRef (r,None) ->
           Inl (ArgArg (evaluable_of_global_reference ist.genv r,None))
       | GVar id ->
-          let r = evaluable_of_global_reference ist.genv (VarRef id) in
+          let r = evaluable_of_global_reference ist.genv (GlobRef.VarRef id) in
           Inl (ArgArg (r,None))
       | _ ->
           let bound_names = Glob_ops.bound_glob_vars c in
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index 8ddf17ca14..c252372f21 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -22,7 +22,6 @@ open Util
 open Names
 open Nameops
 open Libnames
-open Globnames
 open Refiner
 open Tacmach.New
 open Tactic_debug
@@ -369,14 +368,14 @@ let interp_reference ist env sigma = function
     try try_interp_ltac_var (coerce_to_reference sigma) ist (Some (env,sigma)) (make ?loc id)
     with Not_found ->
       try
-        VarRef (get_id (Environ.lookup_named id env))
+        GlobRef.VarRef (get_id (Environ.lookup_named id env))
       with Not_found -> Nametab.error_global_not_found (qualid_of_ident ?loc id)
 
 let try_interp_evaluable env (loc, id) =
   let v = Environ.lookup_named id env in
   match v with
   | LocalDef _ -> EvalVarRef id
-  | _ -> error_not_evaluable (VarRef id)
+  | _ -> error_not_evaluable (GlobRef.VarRef id)
 
 let interp_evaluable ist env sigma = function
   | ArgArg (r,Some {loc;v=id}) ->
diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml
index 6aec83318c..3b79a130f2 100644
--- a/plugins/omega/coq_omega.ml
+++ b/plugins/omega/coq_omega.ml
@@ -27,7 +27,6 @@ open Tacmach.New
 open Tactics
 open Logic
 open Libnames
-open Globnames
 open Nametab
 open Contradiction
 open Tactypes
@@ -426,11 +425,11 @@ let destructurate_prop sigma t =
     | _, [_;_] when eq_constr c (Lazy.force coq_ge) -> Kapp (Ge,args)
     | _, [_;_] when eq_constr c (Lazy.force coq_gt) -> Kapp (Gt,args)
     | Const (sp,_), args ->
-	Kapp (Other (string_of_path (path_of_global (ConstRef sp))),args)
+        Kapp (Other (string_of_path (path_of_global (GlobRef.ConstRef sp))),args)
     | Construct (csp,_) , args ->
-	Kapp (Other (string_of_path (path_of_global (ConstructRef csp))), args)
+        Kapp (Other (string_of_path (path_of_global (GlobRef.ConstructRef csp))), args)
     | Ind (isp,_), args ->
-	Kapp (Other (string_of_path (path_of_global (IndRef isp))),args)
+        Kapp (Other (string_of_path (path_of_global (GlobRef.IndRef isp))),args)
     | Var id,[] -> Kvar id
     | Prod ({binder_name=Anonymous},typ,body), [] -> Kimp(typ,body)
     | Prod ({binder_name=Name _},_,_),[] -> CErrors.user_err Pp.(str "Omega: Not a quantifier-free goal")
diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml
index 9973f2ec1d..eb75fca0a1 100644
--- a/plugins/setoid_ring/newring.ml
+++ b/plugins/setoid_ring/newring.ml
@@ -49,7 +49,7 @@ let global_head_of_constr sigma c =
 
 let global_of_constr_nofail c = 
   try global_of_constr c
-  with Not_found -> VarRef (Id.of_string "dummy")
+  with Not_found -> GlobRef.VarRef (Id.of_string "dummy")
 
 let rec mk_clos_but f_map n t =
   let (f, args) = Constr.decompose_appvect t in
diff --git a/plugins/ssr/ssrbwd.ml b/plugins/ssr/ssrbwd.ml
index f0ae90beca..ca92d70263 100644
--- a/plugins/ssr/ssrbwd.ml
+++ b/plugins/ssr/ssrbwd.ml
@@ -12,7 +12,6 @@
 
 open Printer
 open Pretyping
-open Globnames
 open Glob_term
 open Tacmach
 
@@ -47,7 +46,7 @@ let interp_agen ist gl ((goclr, _), (k, gc as c)) (clr, rcs) =
     let loc = rc.CAst.loc in
     match DAst.get rc with
     | GVar id when not_section_id id -> SsrHyp (Loc.tag ?loc id) :: clr', rcs'
-    | GRef (VarRef id, _) when not_section_id id ->
+    | GRef (Names.GlobRef.VarRef id, _) when not_section_id id ->
         SsrHyp (Loc.tag ?loc id) :: clr', rcs'
     | _ -> clr', rcs'
 
@@ -89,7 +88,7 @@ let pf_match = pf_apply (fun e s c t -> understand_tcc e s ~expected_type:t c)
 let apply_rconstr ?ist t gl =
 (* ppdebug(lazy(str"sigma@apply_rconstr=" ++ pr_evar_map None (project gl))); *)
   let n = match ist, DAst.get t with
-    | None, (GVar id | GRef (VarRef id,_)) -> pf_nbargs gl (EConstr.mkVar id)
+    | None, (GVar id | GRef (Names.GlobRef.VarRef id,_)) -> pf_nbargs gl (EConstr.mkVar id)
     | Some ist, _ -> interp_nbargs ist gl t
     | _ -> anomaly "apply_rconstr without ist and not RVar" in
   let mkRlemma i = mkRApp t (mkRHoles i) in
diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml
index 4c95a92022..33e9f871fd 100644
--- a/plugins/ssr/ssrcommon.ml
+++ b/plugins/ssr/ssrcommon.ml
@@ -181,7 +181,6 @@ let option_assert_get o msg =
 
 (** Constructors for rawconstr *)
 open Glob_term
-open Globnames
 open Decl_kinds
 
 let mkRHole = DAst.make @@ GHole (Evar_kinds.InternalHole, Namegen.IntroAnonymous, None)
@@ -191,14 +190,14 @@ let rec isRHoles cl = match cl with
 | [] -> true
 | c :: l -> match DAst.get c with GHole _ -> isRHoles l | _ -> false
 let mkRApp f args = if args = [] then f else DAst.make @@ GApp (f, args)
-let mkRVar id = DAst.make @@ GRef (VarRef id,None)
+let mkRVar id = DAst.make @@ GRef (GlobRef.VarRef id,None)
 let mkRltacVar id = DAst.make @@ GVar (id)
 let mkRCast rc rt =  DAst.make @@ GCast (rc, CastConv rt)
 let mkRType =  DAst.make @@ GSort (UAnonymous {rigid=true})
 let mkRProp =  DAst.make @@ GSort (UNamed [GProp,0])
 let mkRArrow rt1 rt2 = DAst.make @@ GProd (Anonymous, Explicit, rt1, rt2)
-let mkRConstruct c = DAst.make @@ GRef (ConstructRef c,None)
-let mkRInd mind = DAst.make @@ GRef (IndRef mind,None)
+let mkRConstruct c = DAst.make @@ GRef (GlobRef.ConstructRef c,None)
+let mkRInd mind = DAst.make @@ GRef (GlobRef.IndRef mind,None)
 let mkRLambda n s t = DAst.make @@ GLambda (n, Explicit, s, t)
 
 let rec mkRnat n =
@@ -1543,9 +1542,9 @@ let get g =
 end
 
 let is_construct_ref sigma c r =
-  EConstr.isConstruct sigma c && GlobRef.equal (ConstructRef (fst(EConstr.destConstruct sigma c))) r
-let is_ind_ref sigma c r = EConstr.isInd sigma c && GlobRef.equal (IndRef (fst(EConstr.destInd sigma c))) r
+  EConstr.isConstruct sigma c && GlobRef.equal (GlobRef.ConstructRef (fst(EConstr.destConstruct sigma c))) r
+let is_ind_ref sigma c r = EConstr.isInd sigma c && GlobRef.equal (GlobRef.IndRef (fst(EConstr.destInd sigma c))) r
 let is_const_ref sigma c r =
-  EConstr.isConst sigma c && GlobRef.equal (ConstRef (fst(EConstr.destConst sigma c))) r
+  EConstr.isConst sigma c && GlobRef.equal (GlobRef.ConstRef (fst(EConstr.destConst sigma c))) r
 
 (* vim: set filetype=ocaml foldmethod=marker: *)
diff --git a/plugins/ssrmatching/ssrmatching.ml b/plugins/ssrmatching/ssrmatching.ml
index 7fc1a12b61..17db25660f 100644
--- a/plugins/ssrmatching/ssrmatching.ml
+++ b/plugins/ssrmatching/ssrmatching.ml
@@ -361,7 +361,7 @@ type tpattern = {
 let all_ok _ _ = true
 
 let proj_nparams c =
-  try 1 + Recordops.find_projection_nparams (ConstRef c) with _ -> 0
+  try 1 + Recordops.find_projection_nparams (GlobRef.ConstRef c) with _ -> 0
 
 let isRigid c = match kind c with
   | Prod _ | Sort _ | Lambda _ | Case _ | Fix _ | CoFix _ -> true
@@ -454,7 +454,7 @@ let ungen_upat lhs (sigma, uc, t) u =
 
 let nb_cs_proj_args pc f u =
   let na k =
-    List.length (snd (lookup_canonical_conversion (ConstRef pc, k))).o_TCOMPS in
+    List.length (snd (lookup_canonical_conversion (GlobRef.ConstRef pc, k))).o_TCOMPS in
   let nargs_of_proj t = match kind t with
       | App(_,args) -> Array.length args
       | Proj _ -> 0 (* if splay_app calls expand_projection, this has to be
@@ -928,7 +928,7 @@ let id_of_cpattern (_, (c1, c2), _) =
     Some (qualid_basename qid)
   | _, Some { v = CAppExpl ((_, qid, _), []) } when qualid_is_ident qid ->
     Some (qualid_basename qid)
-  | GRef (VarRef x, _), None -> Some x
+  | GRef (GlobRef.VarRef x, _), None -> Some x
   | _ -> None
 let id_of_Cterm t = match id_of_cpattern t with
   | Some x -> x
@@ -1267,7 +1267,7 @@ let pf_fill_occ_term gl occ t =
   cl, t
 
 let cpattern_of_id id =
-  ' ', (DAst.make @@ GRef (VarRef  id, None), None), Some Geninterp.({ lfun = Id.Map.empty; poly = false; extra = Tacinterp.TacStore.empty })
+  ' ', (DAst.make @@ GRef (GlobRef.VarRef  id, None), None), Some Geninterp.({ lfun = Id.Map.empty; poly = false; extra = Tacinterp.TacStore.empty })
 
 let is_wildcard ((_, (l, r), _) : cpattern) : bool = match DAst.get l, r with
   | _, Some { CAst.v = CHole _ } | GHole _, None -> true
diff --git a/plugins/syntax/numeral.ml b/plugins/syntax/numeral.ml
index 0a1cc8745d..a148a3bc73 100644
--- a/plugins/syntax/numeral.ml
+++ b/plugins/syntax/numeral.ml
@@ -12,7 +12,6 @@ open Pp
 open Util
 open Names
 open Libnames
-open Globnames
 open Constrexpr
 open Constrexpr_ops
 open Notation
@@ -31,7 +30,7 @@ let get_constructors ind =
   let mib,oib = Global.lookup_inductive ind in
   let mc = oib.Declarations.mind_consnames in
   Array.to_list
-    (Array.mapi (fun j c -> ConstructRef (ind, j + 1)) mc)
+    (Array.mapi (fun j c -> GlobRef.ConstructRef (ind, j + 1)) mc)
 
 let qualid_of_ref n =
   n |> Coqlib.lib_ref |> Nametab.shortest_qualid_of_global Id.Set.empty
@@ -40,7 +39,7 @@ let q_option () = qualid_of_ref "core.option.type"
 
 let unsafe_locate_ind q =
   match Nametab.locate q with
-  | IndRef i -> i
+  | GlobRef.IndRef i -> i
   | _ -> raise Not_found
 
 let locate_z () =
@@ -166,7 +165,7 @@ let vernac_numeral_notation local ty f g scope opts =
        { pt_local = local;
          pt_scope = scope;
          pt_interp_info = NumeralNotation o;
-         pt_required = Nametab.path_of_global (IndRef tyc),[];
+         pt_required = Nametab.path_of_global (GlobRef.IndRef tyc),[];
          pt_refs = constructors;
          pt_in_match = true }
   in
diff --git a/plugins/syntax/r_syntax.ml b/plugins/syntax/r_syntax.ml
index 1cbc86b6fe..649b51cb0e 100644
--- a/plugins/syntax/r_syntax.ml
+++ b/plugins/syntax/r_syntax.ml
@@ -10,7 +10,6 @@
 
 open Util
 open Names
-open Globnames
 open Glob_term
 open Bigint
 open Constrexpr
@@ -40,9 +39,9 @@ let positive_kn = MutInd.make2 positive_modpath (Label.make "positive")
 let path_of_xI = ((positive_kn,0),1)
 let path_of_xO = ((positive_kn,0),2)
 let path_of_xH = ((positive_kn,0),3)
-let glob_xI = ConstructRef path_of_xI
-let glob_xO = ConstructRef path_of_xO
-let glob_xH = ConstructRef path_of_xH
+let glob_xI = GlobRef.ConstructRef path_of_xI
+let glob_xO = GlobRef.ConstructRef path_of_xO
+let glob_xH = GlobRef.ConstructRef path_of_xH
 
 let pos_of_bignat ?loc x =
   let ref_xI = DAst.make @@ GRef (glob_xI, None) in
@@ -74,9 +73,9 @@ let z_kn = MutInd.make2 positive_modpath (Label.make "Z")
 let path_of_ZERO = ((z_kn,0),1)
 let path_of_POS = ((z_kn,0),2)
 let path_of_NEG = ((z_kn,0),3)
-let glob_ZERO = ConstructRef path_of_ZERO
-let glob_POS = ConstructRef path_of_POS
-let glob_NEG = ConstructRef path_of_NEG
+let glob_ZERO = GlobRef.ConstructRef path_of_ZERO
+let glob_POS = GlobRef.ConstructRef path_of_POS
+let glob_NEG = GlobRef.ConstructRef path_of_NEG
 
 let z_of_int ?loc n =
   if not (Bigint.equal n zero) then
@@ -104,14 +103,14 @@ let rdefinitions = ["Coq";"Reals";"Rdefinitions"]
 let r_modpath = MPfile (make_dir rdefinitions)
 let r_path = make_path rdefinitions "R"
 
-let glob_IZR = ConstRef (Constant.make2 r_modpath @@ Label.make "IZR")
-let glob_Rmult = ConstRef (Constant.make2 r_modpath @@ Label.make "Rmult")
-let glob_Rdiv = ConstRef (Constant.make2 r_modpath @@ Label.make "Rdiv")
+let glob_IZR = GlobRef.ConstRef (Constant.make2 r_modpath @@ Label.make "IZR")
+let glob_Rmult = GlobRef.ConstRef (Constant.make2 r_modpath @@ Label.make "Rmult")
+let glob_Rdiv = GlobRef.ConstRef (Constant.make2 r_modpath @@ Label.make "Rdiv")
 
 let binintdef = ["Coq";"ZArith";"BinIntDef"]
 let z_modpath = MPdot (MPfile (make_dir binintdef), Label.make "Z")
 
-let glob_pow_pos = ConstRef (Constant.make2 z_modpath @@ Label.make "pow_pos")
+let glob_pow_pos = GlobRef.ConstRef (Constant.make2 z_modpath @@ Label.make "pow_pos")
 
 let r_of_rawnum ?loc (sign,n) =
   let n, f, e = NumTok.(n.int, n.frac, n.exp) in
diff --git a/plugins/syntax/string_notation.ml b/plugins/syntax/string_notation.ml
index bc586acce7..8c0f9a3339 100644
--- a/plugins/syntax/string_notation.ml
+++ b/plugins/syntax/string_notation.ml
@@ -12,7 +12,6 @@ open Pp
 open Util
 open Names
 open Libnames
-open Globnames
 open Constrexpr
 open Constrexpr_ops
 open Notation
@@ -23,7 +22,7 @@ let get_constructors ind =
   let mib,oib = Global.lookup_inductive ind in
   let mc = oib.Declarations.mind_consnames in
   Array.to_list
-    (Array.mapi (fun j c -> ConstructRef (ind, j + 1)) mc)
+    (Array.mapi (fun j c -> GlobRef.ConstructRef (ind, j + 1)) mc)
 
 let qualid_of_ref n =
   n |> Coqlib.lib_ref |> Nametab.shortest_qualid_of_global Id.Set.empty
@@ -92,7 +91,7 @@ let vernac_string_notation local ty f g scope =
        { pt_local = local;
          pt_scope = scope;
          pt_interp_info = StringNotation o;
-         pt_required = Nametab.path_of_global (IndRef tyc),[];
+         pt_required = Nametab.path_of_global (GlobRef.IndRef tyc),[];
          pt_refs = constructors;
          pt_in_match = true }
   in