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

7 files changed, 62 insertions, 58 deletions

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 8573dccdf9..c8ea4d6248 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -16,7 +16,6 @@ open Names
 open Nameops
 open Termops
 open Libnames
-open Globnames
 open Namegen
 open Impargs
 open CAst
@@ -361,7 +360,7 @@ let mkPat ?loc qid l = CAst.make ?loc @@
   if List.is_empty l then CPatAtom (Some qid) else CPatCstr (qid,None,l)
 
 let pattern_printable_in_both_syntax (ind,_ as c) =
-  let impl_st = extract_impargs_data (implicits_of_global (ConstructRef c)) in
+  let impl_st = extract_impargs_data (implicits_of_global (GlobRef.ConstructRef c)) in
   let nb_params = Inductiveops.inductive_nparams (Global.env()) ind in
   List.exists (fun (_,impls) ->
     (List.length impls >= nb_params) &&
@@ -416,7 +415,7 @@ let rec extern_cases_pattern_in_scope (custom,scopes as allscopes) vars pat =
 		          (* we don't want to have 'x := _' in our patterns *)
                           acc
 		       | Some c, _ ->
-                          ((extern_reference ?loc Id.Set.empty (ConstRef c), pat) :: acc)
+                          ((extern_reference ?loc Id.Set.empty (GlobRef.ConstRef c), pat) :: acc)
                        | _ -> raise No_match in
                      ip q tail acc
 	          | _ -> assert false
@@ -424,14 +423,14 @@ let rec extern_cases_pattern_in_scope (custom,scopes as allscopes) vars pat =
 	      CPatRecord(List.rev (ip projs args []))
 	    with
 		Not_found | No_match | Exit ->
-                  let c = extern_reference Id.Set.empty (ConstructRef cstrsp) in
+                  let c = extern_reference Id.Set.empty (GlobRef.ConstructRef cstrsp) in
                   if Constrintern.get_asymmetric_patterns () then
 		    if pattern_printable_in_both_syntax cstrsp
 		    then CPatCstr (c, None, args)
 		    else CPatCstr (c, Some (add_patt_for_params (fst cstrsp) args), [])
 		  else
 		    let full_args = add_patt_for_params (fst cstrsp) args in
-		    match drop_implicits_in_patt (ConstructRef cstrsp) 0 full_args with
+                    match drop_implicits_in_patt (GlobRef.ConstructRef cstrsp) 0 full_args with
 		      | Some true_args -> CPatCstr (c, None, true_args)
 		      | None           -> CPatCstr (c, Some full_args, [])
           in
@@ -500,7 +499,7 @@ and extern_notation_pattern allscopes vars t = function
       match DAst.get t with
         | PatCstr (cstr,args,na) ->
           let t = if na = Anonymous then t else DAst.make ?loc (PatCstr (cstr,args,Anonymous)) in
-	  let p = apply_notation_to_pattern ?loc (ConstructRef cstr)
+          let p = apply_notation_to_pattern ?loc (GlobRef.ConstructRef cstr)
             (match_notation_constr_cases_pattern t pat) allscopes vars keyrule in
 	  insert_pat_alias ?loc p na
 	| PatVar Anonymous -> CAst.make ?loc @@ CPatAtom None
@@ -513,7 +512,7 @@ let rec extern_notation_ind_pattern allscopes vars ind args = function
   | (keyrule,pat,n as _rule)::rules ->
     try
       if is_inactive_rule keyrule then raise No_match;
-      apply_notation_to_pattern (IndRef ind)
+      apply_notation_to_pattern (GlobRef.IndRef ind)
         (match_notation_constr_ind_pattern ind args pat) allscopes vars keyrule
     with
         No_match -> extern_notation_ind_pattern allscopes vars ind args rules
@@ -522,7 +521,7 @@ let extern_ind_pattern_in_scope (custom,scopes as allscopes) vars ind args =
   (* pboutill: There are letins in pat which is incompatible with notations and
      not explicit application. *)
   if !Flags.in_debugger||Inductiveops.inductive_has_local_defs (Global.env()) ind then
-    let c = extern_reference vars (IndRef ind) in
+    let c = extern_reference vars (GlobRef.IndRef ind) in
     let args = List.map (extern_cases_pattern_in_scope allscopes vars) args in
     CAst.make @@ CPatCstr (c, Some (add_patt_for_params ind args), [])
   else
@@ -531,9 +530,9 @@ let extern_ind_pattern_in_scope (custom,scopes as allscopes) vars ind args =
       extern_notation_ind_pattern allscopes vars ind args
           (uninterp_ind_pattern_notations ind)
     with No_match ->
-      let c = extern_reference vars (IndRef ind) in
+      let c = extern_reference vars (GlobRef.IndRef ind) in
       let args = List.map (extern_cases_pattern_in_scope allscopes vars) args in
-      match drop_implicits_in_patt (IndRef ind) 0 args with
+      match drop_implicits_in_patt (GlobRef.IndRef ind) 0 args with
 	   |Some true_args -> CAst.make @@ CPatCstr (c, None, true_args)
 	   |None           -> CAst.make @@ CPatCstr (c, Some args, [])
 
@@ -825,7 +824,7 @@ let rec extern inctx scopes vars r =
 	     begin
 	       try
                  if !Flags.raw_print then raise Exit;
-		 let cstrsp = match ref with ConstructRef c -> c | _ -> raise Not_found in
+                 let cstrsp = match ref with GlobRef.ConstructRef c -> c | _ -> raise Not_found in
 		 let struc = Recordops.lookup_structure (fst cstrsp) in
                  if PrintingRecord.active (fst cstrsp) then
                    ()
@@ -858,7 +857,7 @@ let rec extern inctx scopes vars r =
 				     (* we give up since the constructor is not complete *)
 				 | (arg, scopes) :: tail ->
                                      let head = extern true scopes vars arg in
-                                     ip q locs' tail ((extern_reference ?loc Id.Set.empty (ConstRef c), head) :: acc)
+                                     ip q locs' tail ((extern_reference ?loc Id.Set.empty (GlobRef.ConstRef c), head) :: acc)
 		   in
 		 CRecord (List.rev (ip projs locals args []))
 	       with
@@ -1238,7 +1237,7 @@ let rec glob_of_pat avoid env sigma pat = DAst.make @@ match pat with
       GVar id
   | PMeta None -> GHole (Evar_kinds.InternalHole, IntroAnonymous,None)
   | PMeta (Some n) -> GPatVar (Evar_kinds.FirstOrderPatVar n)
-  | PProj (p,c) -> GApp (DAst.make @@ GRef (ConstRef (Projection.constant p),None),
+  | PProj (p,c) -> GApp (DAst.make @@ GRef (GlobRef.ConstRef (Projection.constant p),None),
 			 [glob_of_pat avoid env sigma c])
   | PApp (f,args) ->
       GApp (glob_of_pat avoid env sigma f,Array.map_to_list (glob_of_pat avoid env sigma) args)
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 68ade75815..f341071728 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -647,7 +647,7 @@ let terms_of_binders bl =
     | PatVar (Name id)   -> CRef (qualid_of_ident id, None)
     | PatVar (Anonymous) -> error_cannot_coerce_wildcard_term ?loc ()
     | PatCstr (c,l,_) ->
-       let qid = qualid_of_path ?loc (Nametab.path_of_global (ConstructRef c)) in
+       let qid = qualid_of_path ?loc (Nametab.path_of_global (GlobRef.ConstructRef c)) in
        let hole = CAst.make ?loc @@ CHole (None,IntroAnonymous,None) in
        let params = List.make (Inductiveops.inductive_nparams (Global.env()) (fst c)) hole in
        CAppExpl ((None,qid,None),params @ List.map term_of_pat l)) pt in
@@ -951,7 +951,7 @@ let intern_var env (ltacvars,ntnvars) namedctx loc id us =
       try
         (* [id] a section variable *)
         (* Redundant: could be done in intern_qualid *)
-        let ref = VarRef id in
+        let ref = GlobRef.VarRef id in
         let impls = implicits_of_global ref in
         let scopes = find_arguments_scope ref in
         Dumpglob.dump_secvar ?loc id; (* this raises Not_found when not a section variable *)
@@ -1014,7 +1014,7 @@ let glob_sort_of_level (level: glob_level) : glob_sort =
 let intern_qualid ?(no_secvar=false) qid intern env ntnvars us args =
   let loc = qid.loc in
   match intern_extended_global_of_qualid qid with
-  | TrueGlobal (VarRef _) when no_secvar ->
+  | TrueGlobal (GlobRef.VarRef _) when no_secvar ->
       (* Rule out section vars since these should have been found by intern_var *)
       raise Not_found
   | TrueGlobal ref -> (DAst.make ?loc @@ GRef (ref, us)), Some ref, args
@@ -1063,6 +1063,7 @@ let check_applied_projection isproj realref qid =
   match isproj with
   | None -> ()
   | Some projargs ->
+    let open GlobRef in
     let is_prim = match realref with
       | None | Some (IndRef _ | ConstructRef _ | VarRef _) -> false
       | Some (ConstRef c) ->
@@ -1219,7 +1220,9 @@ let insert_local_defs_in_pattern (ind,j) l =
       | _ -> assert false in
     aux decls l
 
-let add_local_defs_and_check_length loc env g pl args = match g with
+let add_local_defs_and_check_length loc env g pl args =
+  let open GlobRef in
+  match g with
   | ConstructRef cstr ->
      (* We consider that no variables corresponding to local binders
         have been given in the "explicit" arguments, which come from a
@@ -1259,14 +1262,14 @@ let add_implicits_check_length fail nargs nargs_with_letin impls_st len_pl1 pl2
 let add_implicits_check_constructor_length env loc c len_pl1 pl2 =
   let nargs = Inductiveops.constructor_nallargs env c in
   let nargs' = Inductiveops.constructor_nalldecls env c in
-  let impls_st = implicits_of_global (ConstructRef c) in
+  let impls_st = implicits_of_global (GlobRef.ConstructRef c) in
   add_implicits_check_length (error_wrong_numarg_constructor ?loc env c)
     nargs nargs' impls_st len_pl1 pl2
 
 let add_implicits_check_ind_length env loc c len_pl1 pl2 =
   let nallargs = inductive_nallargs env c in
   let nalldecls = inductive_nalldecls env c in
-  let impls_st = implicits_of_global (IndRef c) in
+  let impls_st = implicits_of_global (GlobRef.IndRef c) in
   add_implicits_check_length (error_wrong_numarg_inductive ?loc env c)
     nallargs nalldecls impls_st len_pl1 pl2
 
@@ -1283,6 +1286,7 @@ let chop_params_pattern loc ind args with_letin =
   args
 
 let find_constructor loc add_params ref =
+  let open GlobRef in
   let (ind,_ as cstr) = match ref with
   | ConstructRef cstr -> cstr
   | IndRef _ ->
@@ -1317,7 +1321,7 @@ let check_duplicate ?loc fields =
       pr_qualid r ++ str ".")
 
 let inductive_of_record loc record =
-  let inductive = IndRef (inductive_of_constructor record.Recordops.s_CONST) in
+  let inductive = GlobRef.IndRef (inductive_of_constructor record.Recordops.s_CONST) in
   Nametab.shortest_qualid_of_global ?loc Id.Set.empty inductive
 
 (** [sort_fields ~complete loc fields completer] expects a list
@@ -1348,7 +1352,7 @@ let sort_fields ~complete loc fields completer =
         let nparams = record.Recordops.s_EXPECTEDPARAM in
         (* the reference constructor of the record *)
         let base_constructor =
-          let global_record_id = ConstructRef record.Recordops.s_CONST in
+          let global_record_id = GlobRef.ConstructRef record.Recordops.s_CONST in
           try Nametab.shortest_qualid_of_global ?loc Id.Set.empty global_record_id
           with Not_found ->
             anomaly (str "Environment corruption for records.") in
@@ -1363,7 +1367,7 @@ let sort_fields ~complete loc fields completer =
             match projs with
               | [] -> (idx, acc_first_idx, acc)
               | (Some field_glob_id) :: projs ->
-                 let field_glob_ref = ConstRef field_glob_id in
+                 let field_glob_ref = GlobRef.ConstRef field_glob_id in
                  let first_field = GlobRef.equal field_glob_ref first_field_glob_ref in
                  begin match proj_kinds with
                     | [] -> anomaly (Pp.str "Number of projections mismatch.")
@@ -1407,7 +1411,7 @@ let sort_fields ~complete loc fields completer =
                    raise (InternalizationError(loc, NotAProjectionOf (field_ref, inductive_ref)))
                in
                let remaining_projs, (field_index, _) =
-                 let the_proj (idx, glob_id) = GlobRef.equal field_glob_ref (ConstRef glob_id) in
+                 let the_proj (idx, glob_id) = GlobRef.equal field_glob_ref (GlobRef.ConstRef glob_id) in
                  try CList.extract_first the_proj remaining_projs
                  with Not_found ->
                    let ind1 = inductive_of_record loc record in
@@ -1518,12 +1522,12 @@ let drop_notations_pattern looked_for genv =
   let ensure_kind top loc g =
     try
       if top then looked_for g else
-      match g with ConstructRef _ -> () | _ -> raise Not_found
+      match g with GlobRef.ConstructRef _ -> () | _ -> raise Not_found
     with Not_found ->
       error_invalid_pattern_notation ?loc ()
   in
   let test_kind top =
-    if top then looked_for else function ConstructRef _ -> () | _ -> raise Not_found
+    if top then looked_for else function GlobRef.ConstructRef _ -> () | _ -> raise Not_found
   in
   (* [rcp_of_glob] : from [glob_constr] to [raw_cases_pattern_expr] *)
   let rec rcp_of_glob scopes x = DAst.(map (function
@@ -1736,7 +1740,7 @@ let rec intern_pat genv ntnvars aliases pat =
 
 let intern_cases_pattern genv ntnvars scopes aliases pat =
   intern_pat genv ntnvars aliases
-    (drop_notations_pattern (function ConstructRef _ -> () | _ -> raise Not_found) genv scopes pat)
+    (drop_notations_pattern (function GlobRef.ConstructRef _ -> () | _ -> raise Not_found) genv scopes pat)
 
 let _ =
   intern_cases_pattern_fwd :=
@@ -1745,13 +1749,13 @@ let _ =
 let intern_ind_pattern genv ntnvars scopes pat =
   let no_not =
     try
-      drop_notations_pattern (function (IndRef _ | ConstructRef _) -> () | _ -> raise Not_found) genv scopes pat
+      drop_notations_pattern (function (GlobRef.IndRef _ | GlobRef.ConstructRef _) -> () | _ -> raise Not_found) genv scopes pat
     with InternalizationError(loc,NotAConstructor _) -> error_bad_inductive_type ?loc
   in
   let loc = no_not.CAst.loc in
   match DAst.get no_not with
     | RCPatCstr (head, expl_pl, pl) ->
-      let c = (function IndRef ind -> ind | _ -> error_bad_inductive_type ?loc) head in
+      let c = (function GlobRef.IndRef ind -> ind | _ -> error_bad_inductive_type ?loc) head in
       let with_letin, pl2 = add_implicits_check_ind_length genv loc c
 	(List.length expl_pl) pl in
       let idslpl = List.map (intern_pat genv ntnvars empty_alias) (expl_pl@pl2) in
@@ -1790,7 +1794,7 @@ let set_hole_implicit i b c =
       Loc.tag ?loc (Evar_kinds.ImplicitArg (r,i,b),IntroAnonymous,None)
     | _ -> anomaly (Pp.str "Only refs have implicits.")
     end
-  | GVar id -> Loc.tag ?loc (Evar_kinds.ImplicitArg (VarRef id,i,b),IntroAnonymous,None)
+  | GVar id -> Loc.tag ?loc (Evar_kinds.ImplicitArg (GlobRef.VarRef id,i,b),IntroAnonymous,None)
   | _ -> anomaly (Pp.str "Only refs have implicits.")
 
 let exists_implicit_name id =
@@ -2161,7 +2165,7 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
       let loc = tm'.CAst.loc in
       match DAst.get tm', na with
       | GVar id, None when not (Id.Map.mem id (snd lvar)) -> Some id, CAst.make ?loc @@ Name id
-      | GRef (VarRef id, _), None -> Some id, CAst.make ?loc @@ Name id
+      | GRef (GlobRef.VarRef id, _), None -> Some id, CAst.make ?loc @@ Name id
       | _, None -> None, CAst.make Anonymous
       | _, Some ({ CAst.loc; v = na } as lna) -> None, lna in
     (* the "in" part *)
diff --git a/interp/dumpglob.ml b/interp/dumpglob.ml
index dc6a1ae180..9bef31c7d8 100644
--- a/interp/dumpglob.ml
+++ b/interp/dumpglob.ml
@@ -115,12 +115,13 @@ let type_of_global_ref gr =
   if Typeclasses.is_class gr then
     "class"
   else
+    let open Names.GlobRef in
     match gr with
-    | Globnames.ConstRef cst ->
-        type_of_logical_kind (constant_kind cst)
-    | Globnames.VarRef v ->
-	"var" ^ type_of_logical_kind (Decls.variable_kind v)
-    | Globnames.IndRef ind ->
+    | ConstRef cst ->
+      type_of_logical_kind (constant_kind cst)
+    | VarRef v ->
+      "var" ^ type_of_logical_kind (Decls.variable_kind v)
+    | IndRef ind ->
 	let (mib,oib) = Inductive.lookup_mind_specif (Global.env ()) ind in
           if mib.Declarations.mind_record <> Declarations.NotRecord then
             begin match mib.Declarations.mind_finite with
@@ -134,7 +135,7 @@ let type_of_global_ref gr =
             | BiFinite -> "variant"
 	    | CoFinite -> "coind"
             end
-    | Globnames.ConstructRef _ -> "constr"
+    | ConstructRef _ -> "constr"
 
 let remove_sections dir =
   let cwd = Lib.cwd_except_section () in
diff --git a/interp/impargs.ml b/interp/impargs.ml
index 9977b29310..0466efa991 100644
--- a/interp/impargs.ml
+++ b/interp/impargs.ml
@@ -394,18 +394,18 @@ let compute_mib_implicits flags kn =
       (Array.mapi  (* No need to lift, arities contain no de Bruijn *)
         (fun i mip ->
           (* No need to care about constraints here *)
-          let ty, _ = Typeops.type_of_global_in_context env (IndRef (kn,i)) in
+          let ty, _ = Typeops.type_of_global_in_context env (GlobRef.IndRef (kn,i)) in
           let r = Inductive.relevance_of_inductive env (kn,i) in
           Context.Rel.Declaration.LocalAssum (Context.make_annot (Name mip.mind_typename) r, ty))
         mib.mind_packets) in
   let env_ar = Environ.push_rel_context ar env in
   let imps_one_inductive i mip =
     let ind = (kn,i) in
-    let ar, _ = Typeops.type_of_global_in_context env (IndRef ind) in
-    ((IndRef ind,compute_semi_auto_implicits env sigma flags (of_constr ar)),
+    let ar, _ = Typeops.type_of_global_in_context env (GlobRef.IndRef ind) in
+    ((GlobRef.IndRef ind,compute_semi_auto_implicits env sigma flags (of_constr ar)),
      Array.mapi (fun j (ctx, cty) ->
       let c = of_constr (Term.it_mkProd_or_LetIn cty ctx) in
-       (ConstructRef (ind,j+1),compute_semi_auto_implicits env_ar sigma flags c))
+       (GlobRef.ConstructRef (ind,j+1),compute_semi_auto_implicits env_ar sigma flags c))
        mip.mind_nf_lc)
   in
   Array.mapi imps_one_inductive mib.mind_packets
@@ -424,7 +424,7 @@ let compute_var_implicits flags id =
 
 (* Implicits of a global reference. *)
 
-let compute_global_implicits flags = function
+let compute_global_implicits flags = let open GlobRef in function
   | VarRef id -> compute_var_implicits flags id
   | ConstRef kn -> compute_constant_implicits flags kn
   | IndRef (kn,i) ->
@@ -579,11 +579,11 @@ let declare_implicits local ref =
 
 let declare_var_implicits id =
   let flags = !implicit_args in
-    declare_implicits_gen ImplLocal flags (VarRef id)
+    declare_implicits_gen ImplLocal flags (GlobRef.VarRef id)
 
 let declare_constant_implicits con =
   let flags = !implicit_args in
-    declare_implicits_gen (ImplConstant flags) flags (ConstRef con)
+    declare_implicits_gen (ImplConstant flags) flags (GlobRef.ConstRef con)
 
 let declare_mib_implicits kn =
   let flags = !implicit_args in
diff --git a/interp/notation.ml b/interp/notation.ml
index d58125e29b..4a6ed75f10 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -305,7 +305,7 @@ let glob_constr_keys c = match DAst.get c with
   | _ -> [Oth]
 
 let cases_pattern_key c = match DAst.get c with
-  | PatCstr (ref,_,_) -> RefKey (canonical_gr (ConstructRef ref))
+  | PatCstr (ref,_,_) -> RefKey (canonical_gr (GlobRef.ConstructRef ref))
   | _ -> Oth
 
 let notation_constr_key = function (* Rem: NApp(NRef ref,[]) stands for @ref *)
@@ -492,10 +492,10 @@ exception NotAValidPrimToken
     considered for parsing. *)
 
 let rec constr_of_glob env sigma g = match DAst.get g with
-  | Glob_term.GRef (ConstructRef c, _) ->
+  | Glob_term.GRef (GlobRef.ConstructRef c, _) ->
       let sigma,c = Evd.fresh_constructor_instance env sigma c in
       sigma,mkConstructU c
-  | Glob_term.GRef (IndRef c, _) ->
+  | Glob_term.GRef (GlobRef.IndRef c, _) ->
       let sigma,c = Evd.fresh_inductive_instance env sigma c in
       sigma,mkIndU c
   | Glob_term.GApp (gc, gcl) ->
@@ -511,10 +511,10 @@ let rec glob_of_constr token_kind ?loc env sigma c = match Constr.kind c with
       let c = glob_of_constr token_kind ?loc env sigma c in
       let cel = List.map (glob_of_constr token_kind ?loc env sigma) (Array.to_list ca) in
       DAst.make ?loc (Glob_term.GApp (c, cel))
-  | Construct (c, _) -> DAst.make ?loc (Glob_term.GRef (ConstructRef c, None))
-  | Const (c, _) -> DAst.make ?loc (Glob_term.GRef (ConstRef c, None))
-  | Ind (ind, _) -> DAst.make ?loc (Glob_term.GRef (IndRef ind, None))
-  | Var id -> DAst.make ?loc (Glob_term.GRef (VarRef id, None))
+  | Construct (c, _) -> DAst.make ?loc (Glob_term.GRef (GlobRef.ConstructRef c, None))
+  | Const (c, _) -> DAst.make ?loc (Glob_term.GRef (GlobRef.ConstRef c, None))
+  | Ind (ind, _) -> DAst.make ?loc (Glob_term.GRef (GlobRef.IndRef ind, None))
+  | Var id -> DAst.make ?loc (Glob_term.GRef (GlobRef.VarRef id, None))
   | Int i -> DAst.make ?loc (Glob_term.GInt i)
   | _ -> Loc.raise ?loc (PrimTokenNotationError(token_kind,env,sigma,UnexpectedTerm c))
 
@@ -836,7 +836,7 @@ let q_byte () = qualid_of_ref "core.byte.type"
 
 let unsafe_locate_ind q =
   match Nametab.locate q with
-  | IndRef i -> i
+  | GlobRef.IndRef i -> i
   | _ -> raise Not_found
 
 let locate_list () = unsafe_locate_ind (q_list ())
@@ -1219,7 +1219,7 @@ let uninterp_cases_pattern_notations c =
   keymap_find (cases_pattern_key c) !notations_key_table
 
 let uninterp_ind_pattern_notations ind =
-  keymap_find (RefKey (canonical_gr (IndRef ind))) !notations_key_table
+  keymap_find (RefKey (canonical_gr (GlobRef.IndRef ind))) !notations_key_table
 
 let availability_of_notation (ntn_scope,ntn) scopes =
   let f scope =
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index fdf12faa04..2fa78bb9f3 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -781,7 +781,7 @@ let rec pat_binder_of_term t = DAst.map (function
   | GVar id -> PatVar (Name id)
   | GApp (t, l) ->
     begin match DAst.get t with
-    | GRef (ConstructRef cstr,_) ->
+    | GRef (GlobRef.ConstructRef cstr,_) ->
      let nparams = Inductiveops.inductive_nparams (Global.env()) (fst cstr) in
      let _,l = List.chop nparams l in
      PatCstr (cstr, List.map pat_binder_of_term l, Anonymous)
@@ -1337,10 +1337,10 @@ let rec match_cases_pattern metas (terms,termlists,(),() as sigma) a1 a2 =
  match DAst.get a1, a2 with
   | r1, NVar id2 when Id.List.mem_assoc id2 metas -> (bind_env_cases_pattern sigma id2 a1),(0,[])
   | PatVar Anonymous, NHole _ -> sigma,(0,[])
-  | PatCstr ((ind,_ as r1),largs,Anonymous), NRef (ConstructRef r2) when eq_constructor r1 r2 ->
+  | PatCstr ((ind,_ as r1),largs,Anonymous), NRef (GlobRef.ConstructRef r2) when eq_constructor r1 r2 ->
       let l = try add_patterns_for_params_remove_local_defs (Global.env ()) r1 largs with Not_found -> raise No_match in
       sigma,(0,l)
-  | PatCstr ((ind,_ as r1),args1,Anonymous), NApp (NRef (ConstructRef r2),l2)
+  | PatCstr ((ind,_ as r1),args1,Anonymous), NApp (NRef (GlobRef.ConstructRef r2),l2)
       when eq_constructor r1 r2 ->
       let l1 = try add_patterns_for_params_remove_local_defs (Global.env()) r1 args1 with Not_found -> raise No_match in
       let le2 = List.length l2 in
@@ -1362,9 +1362,9 @@ and match_cases_pattern_no_more_args metas sigma a1 a2 =
 
 let match_ind_pattern metas sigma ind pats a2 =
   match a2 with
-  | NRef (IndRef r2) when eq_ind ind r2 ->
+  | NRef (GlobRef.IndRef r2) when eq_ind ind r2 ->
       sigma,(0,pats)
-  | NApp (NRef (IndRef r2),l2)
+  | NApp (NRef (GlobRef.IndRef r2),l2)
       when eq_ind ind r2 ->
       let le2 = List.length l2 in
       if Int.equal le2 0 (* Special case of a notation for a @Cstr *) || le2 > List.length pats
diff --git a/interp/smartlocate.ml b/interp/smartlocate.ml
index 74fe5d1c80..5d36ceca38 100644
--- a/interp/smartlocate.ml
+++ b/interp/smartlocate.ml
@@ -52,7 +52,7 @@ let locate_global_with_alias ?(head=false) qid =
 
 let global_inductive_with_alias qid  =
   try match locate_global_with_alias qid with
-  | IndRef ind -> ind
+  | Names.GlobRef.IndRef ind -> ind
   | ref ->
       user_err ?loc:qid.CAst.loc ~hdr:"global_inductive"
         (pr_qualid qid ++ spc () ++ str "is not an inductive type.")