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

14 files changed, 73 insertions, 76 deletions

diff --git a/pretyping/arguments_renaming.ml b/pretyping/arguments_renaming.ml
index 47916ffb79..534c0ca20b 100644
--- a/pretyping/arguments_renaming.ml
+++ b/pretyping/arguments_renaming.ml
@@ -91,23 +91,23 @@ let rename_type ty ref =
 
 let rename_type_of_constant env c =
   let ty = Typeops.type_of_constant_in env c in
-  rename_type ty (ConstRef (fst c))
+  rename_type ty (GlobRef.ConstRef (fst c))
 
 let rename_type_of_inductive env ind =
   let ty = Inductiveops.type_of_inductive env ind in
-  rename_type ty (IndRef (fst ind))
+  rename_type ty (GlobRef.IndRef (fst ind))
 
 let rename_type_of_constructor env cstruct =
   let ty = Inductiveops.type_of_constructor env cstruct in
-  rename_type ty (ConstructRef (fst cstruct))
+  rename_type ty (GlobRef.ConstructRef (fst cstruct))
 
 let rename_typing env c =
   let j = Typeops.infer env c in
   let j' =
     match kind c with
-    | Const (c,u) -> { j with uj_type = rename_type j.uj_type (ConstRef c) }
-    | Ind (i,u) -> { j with uj_type = rename_type j.uj_type (IndRef i) }
-    | Construct (k,u) -> { j with uj_type = rename_type j.uj_type (ConstructRef k) }
+    | Const (c,u) -> { j with uj_type = rename_type j.uj_type (GlobRef.ConstRef c) }
+    | Ind (i,u) -> { j with uj_type = rename_type j.uj_type (GlobRef.IndRef i) }
+    | Construct (k,u) -> { j with uj_type = rename_type j.uj_type (GlobRef.ConstructRef k) }
     | _ -> j
   in j'
 
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 20dec96ef4..a562204b54 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -367,7 +367,7 @@ let make_return_predicate_ltac_lvar env sigma na tm c =
      - if [c] is a variable [id'], then [x] should now become [id']
      - otherwise, [x] should be hidden *)
   match na, DAst.get tm with
-  | Name id, (GVar id' | GRef (Globnames.VarRef id', _)) when Id.equal id id' ->
+  | Name id, (GVar id' | GRef (GlobRef.VarRef id', _)) when Id.equal id id' ->
      let expansion = match kind sigma c with
        | Var id' -> Name id'
        | _ -> Anonymous in
diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index afb546b2d2..1e5c07c061 100644
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
@@ -225,14 +225,14 @@ let string_of_class = function
   | CL_FUN -> "Funclass"
   | CL_SORT -> "Sortclass"
   | CL_CONST sp ->
-    string_of_qualid (Nametab.shortest_qualid_of_global Id.Set.empty (ConstRef sp))
+    string_of_qualid (Nametab.shortest_qualid_of_global Id.Set.empty (GlobRef.ConstRef sp))
   | CL_PROJ sp ->
     let sp = Projection.Repr.constant sp in
-    string_of_qualid (Nametab.shortest_qualid_of_global Id.Set.empty (ConstRef sp))
+    string_of_qualid (Nametab.shortest_qualid_of_global Id.Set.empty (GlobRef.ConstRef sp))
   | CL_IND sp ->
-      string_of_qualid (Nametab.shortest_qualid_of_global Id.Set.empty (IndRef sp))
+      string_of_qualid (Nametab.shortest_qualid_of_global Id.Set.empty (GlobRef.IndRef sp))
   | CL_SECVAR sp ->
-      string_of_qualid (Nametab.shortest_qualid_of_global Id.Set.empty (VarRef sp))
+      string_of_qualid (Nametab.shortest_qualid_of_global Id.Set.empty (GlobRef.VarRef sp))
 
 let pr_class x = str (string_of_class x)
 
@@ -276,8 +276,8 @@ let lookup_path_to_fun_from env sigma s =
 let lookup_path_to_sort_from env sigma s =
   apply_on_class_of env sigma s lookup_path_to_sort_from_class
 
-let mkNamed = function
-  | GlobRef.ConstRef c -> EConstr.mkConst c
+let mkNamed = let open GlobRef in function
+  | ConstRef c -> EConstr.mkConst c
   | VarRef v -> EConstr.mkVar v
   | ConstructRef c -> EConstr.mkConstruct c
   | IndRef i -> EConstr.mkInd i
@@ -325,8 +325,8 @@ let different_class_params env i =
     if (snd ci).cl_param > 0 then true
     else 
       match fst ci with
-      | CL_IND i -> Environ.is_polymorphic env (IndRef i)
-      | CL_CONST c -> Environ.is_polymorphic env (ConstRef c)
+      | CL_IND i -> Environ.is_polymorphic env (GlobRef.IndRef i)
+      | CL_CONST c -> Environ.is_polymorphic env (GlobRef.ConstRef c)
       | _ -> false
 
 let add_coercion_in_graph env sigma (ic,source,target) =
@@ -393,15 +393,15 @@ let reference_arity_length env sigma ref =
   List.length (fst (Reductionops.splay_arity env sigma (EConstr.of_constr t)))
 
 let projection_arity_length env sigma p =
-  let len = reference_arity_length env sigma (ConstRef (Projection.Repr.constant p)) in
+  let len = reference_arity_length env sigma (GlobRef.ConstRef (Projection.Repr.constant p)) in
   len - Projection.Repr.npars p
 
 let class_params env sigma = function
   | CL_FUN | CL_SORT -> 0
-  | CL_CONST sp -> reference_arity_length env sigma (ConstRef sp)
+  | CL_CONST sp -> reference_arity_length env sigma (GlobRef.ConstRef sp)
   | CL_PROJ sp -> projection_arity_length env sigma sp
-  | CL_SECVAR sp -> reference_arity_length env sigma (VarRef sp)
-  | CL_IND sp  -> reference_arity_length env sigma (IndRef sp)
+  | CL_SECVAR sp -> reference_arity_length env sigma (GlobRef.VarRef sp)
+  | CL_IND sp  -> reference_arity_length env sigma (GlobRef.IndRef sp)
 
 (* add_class : cl_typ -> locality_flag option -> bool -> unit *)
 
diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml
index 415b9ec6df..e85c888b2e 100644
--- a/pretyping/constr_matching.ml
+++ b/pretyping/constr_matching.ml
@@ -15,7 +15,6 @@ open Util
 open Names
 open Constr
 open Context
-open Globnames
 open Termops
 open EConstr
 open Vars
@@ -237,11 +236,12 @@ let merge_binding sigma allow_bound_rels ctx n cT subst =
       else raise PatternMatchingFailure
   in
   constrain sigma n c subst
-      
+
 let matches_core env sigma allow_bound_rels
     (binding_vars,pat) c =
   let open EConstr in
-  let convref ref c = 
+  let convref ref c =
+    let open GlobRef in
     match ref, EConstr.kind sigma c with
     | VarRef id, Var id' -> Names.Id.equal id id'
     | ConstRef c, Const (c',_) -> Constant.equal c c'
@@ -270,7 +270,7 @@ let matches_core env sigma allow_bound_rels
 
       | PMeta None, m -> subst
 
-      | PRef (VarRef v1), Var v2 when Id.equal v1 v2 -> subst
+      | PRef (GlobRef.VarRef v1), Var v2 when Id.equal v1 v2 -> subst
 
       | PVar v1, Var v2 when Id.equal v1 v2 -> subst
 
@@ -307,7 +307,7 @@ let matches_core env sigma allow_bound_rels
 	   
       | PApp (c1,arg1), App (c2,arg2) ->
 	(match c1, EConstr.kind sigma c2 with
-	| PRef (ConstRef r), Proj (pr,c) when not (Constant.equal r (Projection.constant pr))
+        | PRef (GlobRef.ConstRef r), Proj (pr,c) when not (Constant.equal r (Projection.constant pr))
 	    || Projection.unfolded pr ->
 	  raise PatternMatchingFailure
 	| PProj (pr1,c1), Proj (pr,c) ->
@@ -323,7 +323,7 @@ let matches_core env sigma allow_bound_rels
           try Array.fold_left2 (sorec ctx env) (sorec ctx env subst c1 c2) arg1 arg2
           with Invalid_argument _ -> raise PatternMatchingFailure)
 	  
-      | PApp (PRef (ConstRef c1), _), Proj (pr, c2) 
+      | PApp (PRef (GlobRef.ConstRef c1), _), Proj (pr, c2)
 	when Projection.unfolded pr || not (Constant.equal c1 (Projection.constant pr)) -> 
 	raise PatternMatchingFailure
 	
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 0daf1ab531..2061b41292 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -185,7 +185,7 @@ module PrintingInductiveMake =
     module Set = Indset
     let encode = Test.encode
     let subst subst obj = subst_ind subst obj
-    let printer ind = Nametab.pr_global_env Id.Set.empty (IndRef ind)
+    let printer ind = Nametab.pr_global_env Id.Set.empty (GlobRef.IndRef ind)
     let key = ["Printing";Test.field]
     let title = Test.title
     let member_message x = Test.member_message (printer x)
@@ -746,7 +746,7 @@ and detype_r d flags avoid env sigma t =
 	  GEvar (Id.of_string_soft ("M" ^ string_of_int n), [])
     | Var id ->
         (* Discriminate between section variable and non-section variable *)
-	(try let _ = Global.lookup_named id in GRef (VarRef id, None)
+        (try let _ = Global.lookup_named id in GRef (GlobRef.VarRef id, None)
 	 with Not_found -> GVar id)
     | Sort s -> GSort (detype_sort sigma (ESorts.kind sigma s))
     | Cast (c1,REVERTcast,c2) when not !Flags.raw_print ->
@@ -772,20 +772,20 @@ and detype_r d flags avoid env sigma t =
       in
       mkapp (detype d flags avoid env sigma f)
         (Array.map_to_list (detype d flags avoid env sigma) args)
-    | Const (sp,u) -> GRef (ConstRef sp, detype_instance sigma u)
+    | Const (sp,u) -> GRef (GlobRef.ConstRef sp, detype_instance sigma u)
     | Proj (p,c) ->
       let noparams () =
         let pars = Projection.npars p in
         let hole = DAst.make @@ GHole(Evar_kinds.InternalHole,Namegen.IntroAnonymous,None) in
         let args = List.make pars hole in
-        GApp (DAst.make @@ GRef (ConstRef (Projection.constant p), None),
+        GApp (DAst.make @@ GRef (GlobRef.ConstRef (Projection.constant p), None),
               (args @ [detype d flags avoid env sigma c]))
       in
       if flags.flg_lax || !Flags.in_debugger || !Flags.in_toplevel then
 	try noparams ()
 	with _ ->
 	    (* lax mode, used by debug printers only *) 
-	  GApp (DAst.make @@ GRef (ConstRef (Projection.constant p), None), 
+          GApp (DAst.make @@ GRef (GlobRef.ConstRef (Projection.constant p), None),
 		[detype d flags avoid env sigma c])
       else 
         if print_primproj_params () then
@@ -821,9 +821,9 @@ and detype_r d flags avoid env sigma t =
         GEvar (id,
                List.map (on_snd (detype d flags avoid env sigma)) l)
     | Ind (ind_sp,u) ->
-	GRef (IndRef ind_sp, detype_instance sigma u)
+        GRef (GlobRef.IndRef ind_sp, detype_instance sigma u)
     | Construct (cstr_sp,u) ->
-	GRef (ConstructRef cstr_sp, detype_instance sigma u)
+        GRef (GlobRef.ConstructRef cstr_sp, detype_instance sigma u)
     | Case (ci,p,c,bl) ->
 	let comp = computable sigma p (List.length (ci.ci_pp_info.ind_tags)) in
 	detype_case comp (detype d flags avoid env sigma)
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index edc948eb65..a82eff9cf0 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -263,7 +263,7 @@ let check_conv_record env sigma (t1,sk1) (t2,sk2) =
 	lookup_canonical_conversion
 	  (proji, Sort_cs (Sorts.family s)),[]
       | Proj (p, c) ->
-        let c2 = Globnames.ConstRef (Projection.constant p) in
+        let c2 = GlobRef.ConstRef (Projection.constant p) in
         let c = Retyping.expand_projection env sigma p c [] in
         let _, args = destApp sigma c in
         let sk2 = Stack.append_app args sk2 in
diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml
index ea94305dd8..6bde3dfd81 100644
--- a/pretyping/glob_ops.ml
+++ b/pretyping/glob_ops.ml
@@ -12,7 +12,6 @@ open Util
 open CAst
 open Names
 open Nameops
-open Globnames
 open Glob_term
 open Evar_kinds
 
@@ -443,7 +442,7 @@ let rec rename_glob_vars l c = force @@ DAst.map_with_loc (fun ?loc -> function
   | GVar id as r ->
       let id' = rename_var l id in
       if id == id' then r else GVar id'
-  | GRef (VarRef id,_) as r ->
+  | GRef (GlobRef.VarRef id,_) as r ->
       if List.exists (fun (_,id') -> Id.equal id id') l then raise UnsoundRenaming
       else r
   | GProd (na,bk,t,c) ->
@@ -502,10 +501,10 @@ let rec cases_pattern_of_glob_constr env na c =
     | Anonymous -> PatVar (Name id)
     end
   | GHole (_,_,_) -> PatVar na
-  | GRef (ConstructRef cstr,_) -> PatCstr (cstr,[],na)
+  | GRef (GlobRef.ConstructRef cstr,_) -> PatCstr (cstr,[],na)
   | GApp (c, l) ->
     begin match DAst.get c with
-    | GRef (ConstructRef cstr,_) ->
+    | GRef (GlobRef.ConstructRef cstr,_) ->
       let nparams = Inductiveops.inductive_nparams env (fst cstr) in
       let _,l = List.chop nparams l in
       PatCstr (cstr,List.map (cases_pattern_of_glob_constr env Anonymous) l,na)
@@ -554,9 +553,9 @@ let add_alias ?loc na c =
 
 (* Turn a closed cases pattern into a glob_constr *)
 let rec glob_constr_of_cases_pattern_aux env isclosed x = DAst.map_with_loc (fun ?loc -> function
-  | PatCstr (cstr,[],na) -> add_alias ?loc na (GRef (ConstructRef cstr,None))
+  | PatCstr (cstr,[],na) -> add_alias ?loc na (GRef (GlobRef.ConstructRef cstr,None))
   | PatCstr (cstr,l,na)  ->
-      let ref = DAst.make ?loc @@ GRef (ConstructRef cstr,None) in
+      let ref = DAst.make ?loc @@ GRef (GlobRef.ConstructRef cstr,None) in
       let l = add_patterns_for_params_remove_local_defs env cstr l in
       add_alias ?loc na (GApp (ref, List.map (glob_constr_of_cases_pattern_aux env isclosed) l))
   | PatVar (Name id) when not isclosed ->
diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml
index e25ebad380..a43549f6c3 100644
--- a/pretyping/indrec.ml
+++ b/pretyping/indrec.ml
@@ -17,7 +17,6 @@ open CErrors
 open Util
 open Names
 open Libnames
-open Globnames
 open Nameops
 open Term
 open Constr
@@ -624,7 +623,7 @@ let lookup_eliminator env ind_sp s =
   try
     let cst = Constant.make knu knc in
     let _ = lookup_constant cst env in
-      ConstRef cst
+      GlobRef.ConstRef cst
   with Not_found ->
   (* Then try to get a user-defined eliminator in some other places *)
   (* using short name (e.g. for "eq_rec") *)
@@ -633,6 +632,6 @@ let lookup_eliminator env ind_sp s =
     user_err ~hdr:"default_elim"
       (strbrk "Cannot find the elimination combinator " ++
        Id.print id ++ strbrk ", the elimination of the inductive definition " ++
-       Nametab.pr_global_env Id.Set.empty (IndRef ind_sp) ++
+       Nametab.pr_global_env Id.Set.empty (GlobRef.IndRef ind_sp) ++
        strbrk " on sort " ++ Sorts.pr_sort_family s ++
        strbrk " is probably not allowed.")
diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml
index 3600f1761b..99e3c5025e 100644
--- a/pretyping/patternops.ml
+++ b/pretyping/patternops.ml
@@ -132,7 +132,7 @@ let rec head_pattern_bound t =
     | PIf (c,_,_)  -> head_pattern_bound c
     | PCase (_,p,c,br) -> head_pattern_bound c
     | PRef r         -> r
-    | PVar id        -> VarRef id
+    | PVar id        -> GlobRef.VarRef id
     | PEvar _ | PRel _ | PMeta _ | PSoApp _  | PSort _ | PFix _ | PProj _
 	-> raise BoundPattern
     (* Perhaps they were arguments, but we don't beta-reduce *)
@@ -140,10 +140,10 @@ let rec head_pattern_bound t =
     | PCoFix _ | PInt _ -> anomaly ~label:"head_pattern_bound" (Pp.str "not a type.")
 
 let head_of_constr_reference sigma c = match EConstr.kind sigma c with
-  | Const (sp,_) -> ConstRef sp
-  | Construct (sp,_) -> ConstructRef sp
-  | Ind (sp,_) -> IndRef sp
-  | Var id -> VarRef id
+  | Const (sp,_) -> GlobRef.ConstRef sp
+  | Construct (sp,_) -> GlobRef.ConstructRef sp
+  | Ind (sp,_) -> GlobRef.IndRef sp
+  | Var id -> GlobRef.VarRef id
   | _ -> anomaly (Pp.str "Not a rigid reference.")
 
 let pattern_of_constr env sigma t =
@@ -175,9 +175,9 @@ let pattern_of_constr env sigma t =
          with
          | Some n -> PSoApp (n,Array.to_list (Array.map (pattern_of_constr env) a))
          | None -> PApp (pattern_of_constr env f,Array.map (pattern_of_constr env) a))
-    | Const (sp,u)  -> PRef (ConstRef (Constant.make1 (Constant.canonical sp)))
-    | Ind (sp,u)    -> PRef (canonical_gr (IndRef sp))
-    | Construct (sp,u) -> PRef (canonical_gr (ConstructRef sp))
+    | Const (sp,u)  -> PRef (GlobRef.ConstRef (Constant.make1 (Constant.canonical sp)))
+    | Ind (sp,u)    -> PRef (canonical_gr (GlobRef.IndRef sp))
+    | Construct (sp,u) -> PRef (canonical_gr (GlobRef.ConstructRef sp))
     | Proj (p, c) -> 
       pattern_of_constr env (EConstr.Unsafe.to_constr (Retyping.expand_projection env sigma p (EConstr.of_constr c) []))
     | Evar (evk,ctxt as ev) ->
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 280b6f9dae..c28c3ab730 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -37,7 +37,6 @@ open Vars
 open Reductionops
 open Type_errors
 open Typing
-open Globnames
 open Evarutil
 open Evardefine
 open Pretype_errors
@@ -435,7 +434,7 @@ let pretype_global ?loc rigid env evd gr us =
 
 let pretype_ref ?loc sigma env ref us =
   match ref with
-  | VarRef id ->
+  | GlobRef.VarRef id ->
       (* Section variable *)
       (try sigma, make_judge (mkVar id) (NamedDecl.get_type (lookup_named id !!env))
        with Not_found ->
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index 1b70119f20..48838a44c4 100644
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -89,11 +89,11 @@ let lookup_structure indsp = Indmap.find indsp !structure_table
 let lookup_projections indsp = (lookup_structure indsp).s_PROJ
 
 let find_projection_nparams = function
-  | ConstRef cst -> (Cmap.find cst !projection_table).s_EXPECTEDPARAM
+  | GlobRef.ConstRef cst -> (Cmap.find cst !projection_table).s_EXPECTEDPARAM
   | _ -> raise Not_found
 
 let find_projection = function
-  | ConstRef cst -> Cmap.find cst !projection_table
+  | GlobRef.ConstRef cst -> Cmap.find cst !projection_table
   | _ -> raise Not_found
 
 let is_projection cst = Cmap.mem cst !projection_table
@@ -185,7 +185,7 @@ let rec cs_pattern_of_constr env t =
   | Proj (p, c) ->
     let { Environ.uj_type = ty } = Typeops.infer env c in
     let _, params = Inductive.find_rectype env ty in
-    Const_cs (ConstRef (Projection.constant p)), None, params @ [c]
+    Const_cs (GlobRef.ConstRef (Projection.constant p)), None, params @ [c]
   | Sort s -> Sort_cs (Sorts.family s), None, []
   | _ -> Const_cs (global_of_constr t) , None, []
 
@@ -193,8 +193,8 @@ let warn_projection_no_head_constant =
   CWarnings.create ~name:"projection-no-head-constant" ~category:"typechecker"
          (fun (sign,env,t,con,proji_sp) ->
           let env = Termops.push_rels_assum sign env in
-          let con_pp = Nametab.pr_global_env Id.Set.empty (ConstRef con) in
-          let proji_sp_pp = Nametab.pr_global_env Id.Set.empty (ConstRef proji_sp) in
+          let con_pp = Nametab.pr_global_env Id.Set.empty (GlobRef.ConstRef con) in
+          let proji_sp_pp = Nametab.pr_global_env Id.Set.empty (GlobRef.ConstRef proji_sp) in
           let term_pp = Termops.Internal.print_constr_env env (Evd.from_env env) (EConstr.of_constr t) in
           strbrk "Projection value has no head constant: "
           ++ term_pp ++ strbrk " in canonical instance "
@@ -223,7 +223,7 @@ let compute_canonical_projections env ~warn (con,ind) =
         Option.cata (fun proji_sp ->
             match cs_pattern_of_constr nenv t with
             | patt, o_INJ, o_TCOMPS ->
-              ((ConstRef proji_sp, (patt, t)),
+              ((GlobRef.ConstRef proji_sp, (patt, t)),
                { o_DEF ; o_CTX ; o_INJ ; o_TABS ; o_TPARAMS ; o_NPARAMS ; o_TCOMPS })
               :: acc
             | exception Not_found ->
@@ -281,7 +281,7 @@ let error_not_structure ref description =
 let check_and_decompose_canonical_structure env sigma ref =
   let sp =
     match ref with
-      ConstRef sp -> sp
+      GlobRef.ConstRef sp -> sp
     |  _ -> error_not_structure ref (str "Expected an instance of a record or structure.")
   in
   let u = Univ.make_abstract_instance (Environ.constant_context env sp) in
@@ -313,13 +313,13 @@ let lookup_canonical_conversion (proj,pat) =
 let decompose_projection sigma c args =
   match EConstr.kind sigma c with
   | Const (c, u) ->
-     let n = find_projection_nparams (ConstRef c) in
+     let n = find_projection_nparams (GlobRef.ConstRef c) in
      (* Check if there is some canonical projection attached to this structure *)
-     let _ = GlobRef.Map.find (ConstRef c) !object_table in
+     let _ = GlobRef.Map.find (GlobRef.ConstRef c) !object_table in
      let arg = Stack.nth args n in
      arg
   | Proj (p, c) ->
-     let _ = GlobRef.Map.find (ConstRef (Projection.constant p)) !object_table in
+     let _ = GlobRef.Map.find (GlobRef.ConstRef (Projection.constant p)) !object_table in
      c
   | _ -> raise Not_found
 
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index d8f01c6bb5..7362955eb7 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -130,7 +130,7 @@ module ReductionBehaviour = struct
     | _ -> None
 
   let rebuild = function
-    | req, (ConstRef c, _ as x) -> req, x
+    | req, (GlobRef.ConstRef c, _ as x) -> req, x
     | _ -> assert false
 
   let inRedBehaviour = declare_object {
@@ -958,7 +958,7 @@ let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma =
           then whrec (if refold then Cst_stack.add_cst (mkConstU const) cst_l else cst_l)
               (body, stack)
           else (* Looks for ReductionBehaviour *)
-            match ReductionBehaviour.get (Globnames.ConstRef c) with
+            match ReductionBehaviour.get (GlobRef.ConstRef c) with
             | None -> whrec (Cst_stack.add_cst (mkConstU const) cst_l) (body, stack)
             | Some behavior ->
               begin match behavior with
@@ -1009,7 +1009,7 @@ let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma =
        if not tactic_mode then
          let stack' = (c, Stack.Proj (p, Cst_stack.empty (*cst_l*)) :: stack) in
          whrec Cst_stack.empty stack'
-       else match ReductionBehaviour.get (Globnames.ConstRef (Projection.constant p)) with
+       else match ReductionBehaviour.get (GlobRef.ConstRef (Projection.constant p)) with
          | None ->
            let stack' = (c, Stack.Proj (p, cst_l) :: stack) in
            let stack'', csts = whrec Cst_stack.empty stack' in
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 6646dfb80c..6fdceb929a 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -67,13 +67,13 @@ let value_of_evaluable_ref env evref u =
   | EvalVarRef id -> env |> lookup_named id |> NamedDecl.get_value |> Option.get
 
 let evaluable_of_global_reference env = function
-  | ConstRef cst when is_evaluable_const env cst -> EvalConstRef cst
-  | VarRef id when is_evaluable_var env id -> EvalVarRef id
+  | GlobRef.ConstRef cst when is_evaluable_const env cst -> EvalConstRef cst
+  | GlobRef.VarRef id when is_evaluable_var env id -> EvalVarRef id
   | r -> error_not_evaluable r
 
 let global_of_evaluable_reference = function
-  | EvalConstRef cst -> ConstRef cst
-  | EvalVarRef id -> VarRef id
+  | EvalConstRef cst -> GlobRef.ConstRef cst
+  | EvalVarRef id -> GlobRef.VarRef id
 
 type evaluable_reference =
   | EvalConst of Constant.t
@@ -597,7 +597,7 @@ let special_red_case env sigma whfun (ci, p, c, lf) =
 
 let recargs = function
   | EvalVar _ | EvalRel _ | EvalEvar _ -> None
-  | EvalConst c -> ReductionBehaviour.get (ConstRef c)
+  | EvalConst c -> ReductionBehaviour.get (GlobRef.ConstRef c)
 
 let reduce_projection env sigma p ~npars (recarg'hd,stack') stack =
   (match EConstr.kind sigma recarg'hd with
@@ -786,7 +786,7 @@ and whd_simpl_stack env sigma =
            let unf = Projection.unfolded p in
            if unf || is_evaluable env (EvalConstRef (Projection.constant p)) then
              let npars = Projection.npars p in
-             (match unf, get (ConstRef (Projection.constant p)) with
+             (match unf, get (GlobRef.ConstRef (Projection.constant p)) with
               | false, Some NeverUnfold -> s'
               | false, Some (UnfoldWhen { recargs } | UnfoldWhenNoMatch { recargs })
                 when not (List.is_empty recargs) ->
@@ -1101,7 +1101,7 @@ let string_of_evaluable_ref env = function
   | EvalVarRef id -> Id.to_string id
   | EvalConstRef kn ->
       string_of_qualid
-        (Nametab.shortest_qualid_of_global (vars_of_env env) (ConstRef kn))
+        (Nametab.shortest_qualid_of_global (vars_of_env env) (GlobRef.ConstRef kn))
 
 let unfold env sigma name c =
   if is_evaluable env name then
@@ -1285,7 +1285,7 @@ let reduce_to_ref_gen allow_product env sigma ref t =
   if isIndRef ref then
     let ((mind,u),t) = reduce_to_ind_gen allow_product env sigma t in
     begin match ref with
-    | IndRef mind' when eq_ind mind mind' -> t
+    | GlobRef.IndRef mind' when eq_ind mind mind' -> t
     | _ -> error_cannot_recognize ref
     end
   else
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index 1d3e77452f..544fd3d17d 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -205,7 +205,7 @@ let build_subclasses ~check env sigma glob { hint_priority = pri } =
 		   | Some p, None -> Some (p + 1)
 		   | _, _ -> None
 		 in
-		   Some (ConstRef proj, { info with hint_priority = newpri }, body)) tc.cl_projs
+                   Some (GlobRef.ConstRef proj, { info with hint_priority = newpri }, body)) tc.cl_projs
 	in
 	let declare_proj hints (cref, info, body) =
 	  let path' = cref :: path in
@@ -243,11 +243,11 @@ let instance_constructor (cl,u) args =
   let open EConstr in
   let pars = fst (List.chop lenpars args) in
     match cl.cl_impl with
-      | IndRef ind -> 
+      | GlobRef.IndRef ind ->
         let ind = ind, u in
           (Some (applist (mkConstructUi (ind, 1), args)),
            applist (mkIndU ind, pars))
-      | ConstRef cst -> 
+      | GlobRef.ConstRef cst ->
         let cst = cst, u in
 	let term = match args with
 	  | [] -> None