Merge PR #7797: Remove reference name type.

11 files changed, 100 insertions, 110 deletions

diff --git a/vernac/classes.ml b/vernac/classes.ml
index 8cf3895fb..382d18b09 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -229,10 +229,7 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance)
             let sigma, c = interp_casted_constr_evars env' sigma term cty in
             Some (Inr (c, subst)), sigma
 	| Some (Inl props) ->
-            let get_id = CAst.map (function
-                | Ident id' -> id'
-                | Qualid id' -> snd (repr_qualid id'))
-	    in
+            let get_id qid = CAst.make ?loc:qid.CAst.loc @@ qualid_basename qid in
 	    let props, rest =
 	      List.fold_left
 		(fun (props, rest) decl ->
diff --git a/vernac/classes.mli b/vernac/classes.mli
index eea2a211d..bd30b2d60 100644
--- a/vernac/classes.mli
+++ b/vernac/classes.mli
@@ -22,7 +22,7 @@ val mismatched_props : env -> constr_expr list -> Context.Rel.t -> 'a
 
 (** Instance declaration *)
 
-val existing_instance : bool -> reference -> Hints.hint_info_expr option -> unit
+val existing_instance : bool -> qualid -> Hints.hint_info_expr option -> unit
 (** globality, reference, optional priority and pattern information *)
 
 val declare_instance_constant :
diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml
index b93e8d9ac..6057c05f5 100644
--- a/vernac/comInductive.ml
+++ b/vernac/comInductive.ml
@@ -44,8 +44,8 @@ let rec complete_conclusion a cs = CAst.map_with_loc (fun ?loc -> function
         user_err ?loc
          (strbrk"Cannot infer the non constant arguments of the conclusion of "
           ++ Id.print cs ++ str ".");
-      let args = List.map (fun id -> CAst.(make ?loc @@ CRef(make ?loc @@ Ident id,None))) params in
-      CAppExpl ((None,CAst.make ?loc @@ Ident name,None),List.rev args)
+      let args = List.map (fun id -> CAst.(make ?loc @@ CRef(qualid_of_ident ?loc id,None))) params in
+      CAppExpl ((None,qualid_of_ident ?loc name,None),List.rev args)
   | c -> c
   )
 
diff --git a/vernac/comProgramFixpoint.ml b/vernac/comProgramFixpoint.ml
index a6d7fccf3..eef7afbfb 100644
--- a/vernac/comProgramFixpoint.ml
+++ b/vernac/comProgramFixpoint.ml
@@ -44,7 +44,7 @@ let mkSubset sigma name typ prop =
 
 let sigT = Lazy.from_fun build_sigma_type
 
-let make_qref s = CAst.make @@ Qualid (qualid_of_string s)
+let make_qref s = qualid_of_string s
 let lt_ref = make_qref "Init.Peano.lt"
 
 let rec telescope sigma l =
diff --git a/vernac/egramcoq.ml b/vernac/egramcoq.ml
index 434e836d8..cc9be7b0e 100644
--- a/vernac/egramcoq.ml
+++ b/vernac/egramcoq.ml
@@ -229,7 +229,7 @@ type prod_info = production_level * production_position
 
 type (_, _) entry =
 | TTName : ('self, lname) entry
-| TTReference : ('self, reference) entry
+| TTReference : ('self, qualid) entry
 | TTBigint : ('self, Constrexpr.raw_natural_number) entry
 | TTConstr : prod_info * 'r target -> ('r, 'r) entry
 | TTConstrList : prod_info * Tok.t list * 'r target -> ('r, 'r list) entry
@@ -312,7 +312,7 @@ let interp_entry forpat e = match e with
 
 let cases_pattern_expr_of_name { CAst.loc; v = na } = CAst.make ?loc @@ match na with
   | Anonymous -> CPatAtom None
-  | Name id   -> CPatAtom (Some (CAst.make ?loc @@ Ident id))
+  | Name id   -> CPatAtom (Some (qualid_of_ident ?loc id))
 
 type 'r env = {
   constrs : 'r list;
diff --git a/vernac/g_vernac.ml4 b/vernac/g_vernac.ml4
index 3a59242de..16934fc86 100644
--- a/vernac/g_vernac.ml4
+++ b/vernac/g_vernac.ml4
@@ -549,7 +549,7 @@ GEXTEND Gram
       ] ]
   ;
   module_expr_atom:
-    [ [ qid = qualid -> CAst.make ~loc:!@loc @@ CMident (qid.CAst.v) | "("; me = module_expr; ")" -> me ] ]
+    [ [ qid = qualid -> CAst.make ~loc:!@loc @@ CMident qid | "("; me = module_expr; ")" -> me ] ]
   ;
   with_declaration:
     [ [ "Definition"; fqid = fullyqualid; udecl = OPT univ_decl; ":="; c = Constr.lconstr ->
@@ -559,7 +559,7 @@ GEXTEND Gram
       ] ]
   ;
   module_type:
-    [ [ qid = qualid -> CAst.make ~loc:!@loc @@ CMident (qid.CAst.v)
+    [ [ qid = qualid -> CAst.make ~loc:!@loc @@ CMident qid
       | "("; mt = module_type; ")" -> mt
       | mty = module_type; me = module_expr_atom ->
           CAst.make ~loc:!@loc @@ CMapply (mty,me)
diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml
index 8f64f5519..da14358ef 100644
--- a/vernac/metasyntax.ml
+++ b/vernac/metasyntax.ml
@@ -1449,7 +1449,7 @@ let add_notation_extra_printing_rule df k v =
 
 (* Infix notations *)
 
-let inject_var x = CAst.make @@ CRef (CAst.make @@ Ident (Id.of_string x),None)
+let inject_var x = CAst.make @@ CRef (qualid_of_ident (Id.of_string x),None)
 
 let add_infix local env ({CAst.loc;v=inf},modifiers) pr sc =
   check_infix_modifiers modifiers;
diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml
index d0c423650..56dfaa54a 100644
--- a/vernac/ppvernac.ml
+++ b/vernac/ppvernac.ml
@@ -16,7 +16,6 @@ open Util
 open CAst
 
 open Extend
-open Libnames
 open Decl_kinds
 open Constrexpr
 open Constrexpr_ops
@@ -79,13 +78,13 @@ open Pputils
   let pr_lname_decl (n, u) =
     pr_lname n ++ pr_universe_decl u
 
-  let pr_smart_global = Pputils.pr_or_by_notation pr_reference
+  let pr_smart_global = Pputils.pr_or_by_notation pr_qualid
 
-  let pr_ltac_ref = Libnames.pr_reference
+  let pr_ltac_ref = Libnames.pr_qualid
 
-  let pr_module = Libnames.pr_reference
+  let pr_module = Libnames.pr_qualid
 
-  let pr_import_module = Libnames.pr_reference
+  let pr_import_module = Libnames.pr_qualid
 
   let sep_end = function
     | VernacBullet _
@@ -157,7 +156,7 @@ open Pputils
   let pr_locality local = if local then keyword "Local" else keyword "Global"
 
   let pr_option_ref_value = function
-    | QualidRefValue id -> pr_reference id
+    | QualidRefValue id -> pr_qualid id
     | StringRefValue s -> qs s
 
   let pr_printoption table b =
@@ -180,7 +179,7 @@ open Pputils
     | _ as z -> str":" ++ spc() ++ prlist_with_sep sep str z
 
   let pr_reference_or_constr pr_c = function
-    | HintsReference r -> pr_reference r
+    | HintsReference r -> pr_qualid r
     | HintsConstr c -> pr_c c
 
   let pr_hint_mode = function
@@ -202,24 +201,24 @@ open Pputils
             l
         | HintsResolveIFF (l2r, l, n) ->
           keyword "Resolve " ++ str (if l2r then "->" else "<-")
-          ++ prlist_with_sep sep pr_reference l
+          ++ prlist_with_sep sep pr_qualid l
         | HintsImmediate l ->
           keyword "Immediate" ++ spc() ++
             prlist_with_sep sep (fun c -> pr_reference_or_constr pr_c c) l
         | HintsUnfold l ->
-          keyword "Unfold" ++ spc () ++ prlist_with_sep sep pr_reference l
+          keyword "Unfold" ++ spc () ++ prlist_with_sep sep pr_qualid l
         | HintsTransparency (l, b) ->
           keyword (if b then "Transparent" else "Opaque")
           ++ spc ()
-          ++ prlist_with_sep sep pr_reference l
+          ++ prlist_with_sep sep pr_qualid l
         | HintsMode (m, l) ->
           keyword "Mode"
           ++ spc ()
-          ++ pr_reference m ++ spc() ++
+          ++ pr_qualid m ++ spc() ++
             prlist_with_sep spc pr_hint_mode l
         | HintsConstructors c ->
           keyword "Constructors"
-          ++ spc() ++ prlist_with_sep spc pr_reference c
+          ++ spc() ++ prlist_with_sep spc pr_qualid c
         | HintsExtern (n,c,tac) ->
           let pat = match c with None -> mt () | Some pat -> pr_pat pat in
           keyword "Extern" ++ spc() ++ int n ++ spc() ++ pat ++ str" =>" ++
@@ -233,7 +232,7 @@ open Pputils
       keyword "Definition" ++ spc() ++ pr_lfqid id ++ pr_universe_decl udecl ++ str" := " ++ p
     | CWith_Module (id,qid) ->
       keyword "Module" ++ spc() ++ pr_lfqid id ++ str" := " ++
-        pr_ast pr_qualid qid
+        pr_qualid qid
 
   let rec pr_module_ast leading_space pr_c = function
     | { loc ; v = CMident qid } ->
@@ -451,7 +450,7 @@ open Pputils
     | PrintFullContext ->
       keyword "Print All"
     | PrintSectionContext s ->
-      keyword "Print Section" ++ spc() ++ Libnames.pr_reference s
+      keyword "Print Section" ++ spc() ++ Libnames.pr_qualid s
     | PrintGrammar ent ->
       keyword "Print Grammar" ++ spc() ++ str ent
     | PrintLoadPath dir ->
@@ -499,9 +498,9 @@ open Pputils
     | PrintName (qid,udecl) ->
       keyword "Print" ++ spc()  ++ pr_smart_global qid ++ pr_univ_name_list udecl
     | PrintModuleType qid ->
-      keyword "Print Module Type" ++ spc() ++ pr_reference qid
+      keyword "Print Module Type" ++ spc() ++ pr_qualid qid
     | PrintModule qid ->
-      keyword "Print Module" ++ spc() ++ pr_reference qid
+      keyword "Print Module" ++ spc() ++ pr_qualid qid
     | PrintInspect n ->
       keyword "Inspect" ++ spc() ++ int n
     | PrintScopes ->
@@ -604,7 +603,7 @@ open Pputils
           | ShowUniverses -> keyword "Show Universes"
           | ShowProofNames -> keyword "Show Conjectures"
           | ShowIntros b -> keyword "Show " ++ (if b then keyword "Intros" else keyword "Intro")
-          | ShowMatch id -> keyword "Show Match " ++ pr_reference id
+          | ShowMatch id -> keyword "Show Match " ++ pr_qualid id
         in
         return (pr_showable s)
       | VernacCheckGuard ->
@@ -901,7 +900,7 @@ open Pputils
 
       | VernacDeclareInstances insts ->
          let pr_inst (id, info) =
-           pr_reference id ++ pr_hint_info pr_constr_pattern_expr info
+           pr_qualid id ++ pr_hint_info pr_constr_pattern_expr info
          in
          return (
           hov 1 (keyword "Existing" ++ spc () ++
@@ -911,7 +910,7 @@ open Pputils
 
       | VernacDeclareClass id ->
         return (
-          hov 1 (keyword "Existing" ++ spc () ++ keyword "Class" ++ spc () ++ pr_reference id)
+          hov 1 (keyword "Existing" ++ spc () ++ keyword "Class" ++ spc () ++ pr_qualid id)
         )
 
       (* Modules and Module Types *)
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 94eb45fd3..479482095 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -183,29 +183,27 @@ let print_modules () =
   pr_vertical_list DirPath.print only_loaded
 
 
-let print_module r =
-  let qid = qualid_of_reference r in
+let print_module qid =
   try
-    let globdir = Nametab.locate_dir qid.v in
+    let globdir = Nametab.locate_dir qid in
       match globdir with
           DirModule { obj_dir; obj_mp; _ } ->
           Printmod.print_module (Printmod.printable_body obj_dir) obj_mp
 	| _ -> raise Not_found
   with
-    Not_found -> user_err (str"Unknown Module " ++ pr_qualid qid.v)
+    Not_found -> user_err (str"Unknown Module " ++ pr_qualid qid)
 
-let print_modtype r =
-  let qid = qualid_of_reference r in
+let print_modtype qid =
   try
-    let kn = Nametab.locate_modtype qid.v in
+    let kn = Nametab.locate_modtype qid in
     Printmod.print_modtype kn
   with Not_found ->
     (* Is there a module of this name ? If yes we display its type *)
     try
-      let mp = Nametab.locate_module qid.v in
+      let mp = Nametab.locate_module qid in
       Printmod.print_module false mp
     with Not_found ->
-      user_err (str"Unknown Module Type or Module " ++ pr_qualid qid.v)
+      user_err (str"Unknown Module Type or Module " ++ pr_qualid qid)
 
 let print_namespace ns =
   let ns = List.rev (Names.DirPath.repr ns) in
@@ -367,33 +365,32 @@ let msg_found_library = function
   | Library.LibInPath, fulldir, file ->
     hov 0 (DirPath.print fulldir ++ strbrk " is bound to file " ++ str file)
 
-let err_unmapped_library ?loc ?from qid =
+let err_unmapped_library ?from qid =
   let dir = fst (repr_qualid qid) in
   let prefix = match from with
   | None -> str "."
   | Some from ->
     str " and prefix " ++ DirPath.print from ++ str "."
   in
-  user_err ?loc
+  user_err ?loc:qid.CAst.loc
     ~hdr:"locate_library"
     (strbrk "Cannot find a physical path bound to logical path matching suffix " ++
        DirPath.print dir ++ prefix)
 
-let err_notfound_library ?loc ?from qid =
+let err_notfound_library ?from qid =
   let prefix = match from with
   | None -> str "."
   | Some from ->
     str " with prefix " ++ DirPath.print from ++ str "."
   in
-  user_err ?loc ~hdr:"locate_library"
+  user_err ?loc:qid.CAst.loc ~hdr:"locate_library"
      (strbrk "Unable to locate library " ++ pr_qualid qid ++ prefix)
 
-let print_located_library r =
-  let {loc;v=qid} = qualid_of_reference r in
+let print_located_library qid =
   try msg_found_library (Library.locate_qualified_library ~warn:false qid)
   with
-    | Library.LibUnmappedDir -> err_unmapped_library ?loc qid
-    | Library.LibNotFound -> err_notfound_library ?loc qid
+    | Library.LibUnmappedDir -> err_unmapped_library qid
+    | Library.LibNotFound -> err_notfound_library qid
 
 let smart_global r =
   let gr = Smartlocate.smart_global r in
@@ -636,7 +633,7 @@ let vernac_scheme l =
 let vernac_combined_scheme lid l =
   if Dumpglob.dump () then
     (Dumpglob.dump_definition lid false "def";
-     List.iter (fun {loc;v=id} -> dump_global (make ?loc @@ AN (make ?loc @@ Ident id))) l);
+     List.iter (fun {loc;v=id} -> dump_global (make ?loc @@ AN (qualid_of_ident ?loc id))) l);
  Indschemes.do_combined_scheme lid l
 
 let vernac_universe ~atts l =
@@ -657,7 +654,7 @@ let vernac_constraint ~atts l =
 (* Modules            *)
 
 let vernac_import export refl =
-  Library.import_module export (List.map qualid_of_reference refl)
+  Library.import_module export refl
 
 let vernac_declare_module export {loc;v=id} binders_ast mty_ast =
   (* We check the state of the system (in section, in module type)
@@ -675,7 +672,7 @@ let vernac_declare_module export {loc;v=id} binders_ast mty_ast =
   in
   Dumpglob.dump_moddef ?loc mp "mod";
   Flags.if_verbose Feedback.msg_info (str "Module " ++ Id.print id ++ str " is declared");
-  Option.iter (fun export -> vernac_import export [make @@ Ident id]) export
+  Option.iter (fun export -> vernac_import export [qualid_of_ident id]) export
 
 let vernac_define_module export {loc;v=id} (binders_ast : module_binder list) mty_ast_o mexpr_ast_l =
   (* We check the state of the system (in section, in module type)
@@ -700,7 +697,7 @@ let vernac_define_module export {loc;v=id} (binders_ast : module_binder list) mt
        List.iter
          (fun (export,id) ->
            Option.iter
-             (fun export -> vernac_import export [make @@ Ident id]) export
+             (fun export -> vernac_import export [qualid_of_ident id]) export
          ) argsexport
     | _::_ ->
        let binders_ast = List.map
@@ -715,14 +712,14 @@ let vernac_define_module export {loc;v=id} (binders_ast : module_binder list) mt
        Dumpglob.dump_moddef ?loc mp "mod";
        Flags.if_verbose Feedback.msg_info
 	 (str "Module " ++ Id.print id ++ str " is defined");
-       Option.iter (fun export -> vernac_import export [make @@ Ident id])
+       Option.iter (fun export -> vernac_import export [qualid_of_ident id])
          export
 
 let vernac_end_module export {loc;v=id} =
   let mp = Declaremods.end_module () in
   Dumpglob.dump_modref ?loc mp "mod";
   Flags.if_verbose Feedback.msg_info (str "Module " ++ Id.print id ++ str " is defined");
-  Option.iter (fun export -> vernac_import export [make ?loc @@ Ident id]) export
+  Option.iter (fun export -> vernac_import export [qualid_of_ident ?loc id]) export
 
 let vernac_declare_module_type {loc;v=id} binders_ast mty_sign mty_ast_l =
   if Lib.sections_are_opened () then
@@ -747,7 +744,7 @@ let vernac_declare_module_type {loc;v=id} binders_ast mty_sign mty_ast_l =
        List.iter
          (fun (export,id) ->
            Option.iter
-             (fun export -> vernac_import export [make ?loc @@ Ident id]) export
+             (fun export -> vernac_import export [qualid_of_ident ?loc id]) export
          ) argsexport
 
     | _ :: _ ->
@@ -809,22 +806,20 @@ let warn_require_in_section =
 
 let vernac_require from import qidl =
   if Lib.sections_are_opened () then warn_require_in_section ();
-  let qidl = List.map qualid_of_reference qidl in
   let root = match from with
   | None -> None
   | Some from ->
-    let qid = Libnames.qualid_of_reference from in
-    let (hd, tl) = Libnames.repr_qualid qid.v in
+    let (hd, tl) = Libnames.repr_qualid from in
     Some (Libnames.add_dirpath_suffix hd tl)
   in
-  let locate {loc;v=qid} =
+  let locate qid =
     try
       let warn = not !Flags.quiet in
       let (_, dir, f) = Library.locate_qualified_library ?root ~warn qid in
       (dir, f)
     with
-      | Library.LibUnmappedDir -> err_unmapped_library ?loc ?from:root qid
-      | Library.LibNotFound -> err_notfound_library ?loc ?from:root qid
+      | Library.LibUnmappedDir -> err_unmapped_library ?from:root qid
+      | Library.LibNotFound -> err_notfound_library ?from:root qid
   in
   let modrefl = List.map locate qidl in
   if Dumpglob.dump () then
@@ -1687,10 +1682,10 @@ let print_about_hyp_globs ?loc ref_or_by_not udecl glopt =
     let glnumopt = query_command_selector ?loc glopt in
     let gl,id =
       match glnumopt, ref_or_by_not.v with
-      | None,AN {v=Ident id} -> (* goal number not given, catch any failure *)
-	 (try get_nth_goal 1,id with _ -> raise NoHyp)
-      | Some n,AN {v=Ident id} ->  (* goal number given, catch if wong *)
-	 (try get_nth_goal n,id
+      | None,AN qid when qualid_is_ident qid -> (* goal number not given, catch any failure *)
+         (try get_nth_goal 1, qualid_basename qid with _ -> raise NoHyp)
+      | Some n,AN qid when qualid_is_ident qid ->  (* goal number given, catch if wong *)
+         (try get_nth_goal n, qualid_basename qid
 	  with
 	    Failure _ -> user_err ?loc ~hdr:"print_about_hyp_globs"
                           (str "No such goal: " ++ int n ++ str "."))
@@ -1771,11 +1766,10 @@ let vernac_print ~atts env sigma =
       Printer.pr_assumptionset env sigma nassums
   | PrintStrategy r -> print_strategy r
 
-let global_module r =
-  let {loc;v=qid} = qualid_of_reference r in
+let global_module qid =
   try Nametab.full_name_module qid
   with Not_found ->
-    user_err ?loc ~hdr:"global_module"
+    user_err ?loc:qid.CAst.loc ~hdr:"global_module"
      (str "Module/section " ++ pr_qualid qid ++ str " not found.")
 
 let interp_search_restriction = function
diff --git a/vernac/vernacentries.mli b/vernac/vernacentries.mli
index 3c88a3443..02a3b2bd6 100644
--- a/vernac/vernacentries.mli
+++ b/vernac/vernacentries.mli
@@ -8,11 +8,11 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-val dump_global : Libnames.reference Constrexpr.or_by_notation -> unit
+val dump_global : Libnames.qualid Constrexpr.or_by_notation -> unit
 
 (** Vernacular entries *)
 val vernac_require :
-  Libnames.reference option -> bool option -> Libnames.reference list -> unit
+  Libnames.qualid option -> bool option -> Libnames.qualid list -> unit
 
 (** The main interpretation function of vernacular expressions *)
 val interp :
diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml
index 5acac9e25..f74383b02 100644
--- a/vernac/vernacexpr.ml
+++ b/vernac/vernacexpr.ml
@@ -13,7 +13,7 @@ open Constrexpr
 open Libnames
 
 (** Vernac expressions, produced by the parser *)
-type class_rawexpr = FunClass | SortClass | RefClass of reference or_by_notation
+type class_rawexpr = FunClass | SortClass | RefClass of qualid or_by_notation
 
 type goal_selector = Goal_select.t =
   | SelectAlreadyFocused
@@ -37,37 +37,37 @@ type univ_name_list = UnivNames.univ_name_list
 type printable =
   | PrintTables
   | PrintFullContext
-  | PrintSectionContext of reference
+  | PrintSectionContext of qualid
   | PrintInspect of int
   | PrintGrammar of string
   | PrintLoadPath of DirPath.t option
   | PrintModules
-  | PrintModule of reference
-  | PrintModuleType of reference
+  | PrintModule of qualid
+  | PrintModuleType of qualid
   | PrintNamespace of DirPath.t
   | PrintMLLoadPath
   | PrintMLModules
   | PrintDebugGC
-  | PrintName of reference or_by_notation * UnivNames.univ_name_list option
+  | PrintName of qualid or_by_notation * UnivNames.univ_name_list option
   | PrintGraph
   | PrintClasses
   | PrintTypeClasses
-  | PrintInstances of reference or_by_notation
+  | PrintInstances of qualid or_by_notation
   | PrintCoercions
   | PrintCoercionPaths of class_rawexpr * class_rawexpr
   | PrintCanonicalConversions
   | PrintUniverses of bool * string option
-  | PrintHint of reference or_by_notation
+  | PrintHint of qualid or_by_notation
   | PrintHintGoal
   | PrintHintDbName of string
   | PrintHintDb
   | PrintScopes
   | PrintScope of string
   | PrintVisibility of string option
-  | PrintAbout of reference or_by_notation * UnivNames.univ_name_list option * Goal_select.t option
-  | PrintImplicit of reference or_by_notation
-  | PrintAssumptions of bool * bool * reference or_by_notation
-  | PrintStrategy of reference or_by_notation option
+  | PrintAbout of qualid or_by_notation * UnivNames.univ_name_list option * Goal_select.t option
+  | PrintImplicit of qualid or_by_notation
+  | PrintAssumptions of bool * bool * qualid or_by_notation
+  | PrintStrategy of qualid or_by_notation option
 
 type search_about_item =
   | SearchSubPattern of constr_pattern_expr
@@ -80,11 +80,11 @@ type searchable =
   | SearchAbout of (bool * search_about_item) list
 
 type locatable =
-  | LocateAny of reference or_by_notation
-  | LocateTerm of reference or_by_notation
-  | LocateLibrary of reference
-  | LocateModule of reference
-  | LocateOther of string * reference
+  | LocateAny of qualid or_by_notation
+  | LocateTerm of qualid or_by_notation
+  | LocateLibrary of qualid
+  | LocateModule of qualid
+  | LocateOther of string * qualid
   | LocateFile of string
 
 type showable =
@@ -95,7 +95,7 @@ type showable =
   | ShowUniverses
   | ShowProofNames
   | ShowIntros of bool
-  | ShowMatch of reference
+  | ShowMatch of qualid
 
 type comment =
   | CommentConstr of constr_expr
@@ -103,7 +103,7 @@ type comment =
   | CommentInt of int
 
 type reference_or_constr = Hints.reference_or_constr =
-  | HintsReference of reference
+  | HintsReference of qualid
   | HintsConstr of constr_expr
 [@@ocaml.deprecated "Please use [Hints.reference_or_constr]"]
 
@@ -123,18 +123,18 @@ type hint_info_expr = Hints.hint_info_expr
 
 type hints_expr = Hints.hints_expr =
   | HintsResolve of (Hints.hint_info_expr * bool * Hints.reference_or_constr) list
-  | HintsResolveIFF of bool * reference list * int option
+  | HintsResolveIFF of bool * qualid list * int option
   | HintsImmediate of Hints.reference_or_constr list
-  | HintsUnfold of reference list
-  | HintsTransparency of reference list * bool
-  | HintsMode of reference * Hints.hint_mode list
-  | HintsConstructors of reference list
+  | HintsUnfold of qualid list
+  | HintsTransparency of qualid list * bool
+  | HintsMode of qualid * Hints.hint_mode list
+  | HintsConstructors of qualid list
   | HintsExtern of int * constr_expr option * Genarg.raw_generic_argument
 [@@ocaml.deprecated "Please use [Hints.hints_expr]"]
 
 type search_restriction =
-  | SearchInside of reference list
-  | SearchOutside of reference list
+  | SearchInside of qualid list
+  | SearchOutside of qualid list
 
 type rec_flag       = bool (* true = Rec;           false = NoRec          *)
 type verbose_flag   = bool (* true = Verbose;       false = Silent         *)
@@ -159,7 +159,7 @@ type option_value = Goptions.option_value =
 
 type option_ref_value =
   | StringRefValue of string
-  | QualidRefValue of reference
+  | QualidRefValue of qualid
 
 (** Identifier and optional list of bound universes and constraints. *)
 
@@ -222,9 +222,9 @@ type proof_end =
   | Proved of Proof_global.opacity_flag * lident option
 
 type scheme =
-  | InductionScheme of bool * reference or_by_notation * sort_expr
-  | CaseScheme of bool * reference or_by_notation * sort_expr
-  | EqualityScheme of reference or_by_notation
+  | InductionScheme of bool * qualid or_by_notation * sort_expr
+  | CaseScheme of bool * qualid or_by_notation * sort_expr
+  | EqualityScheme of qualid or_by_notation
 
 type section_subset_expr =
   | SsEmpty
@@ -348,10 +348,10 @@ type nonrec vernac_expr =
   | VernacBeginSection of lident
   | VernacEndSegment of lident
   | VernacRequire of
-      reference option * export_flag option * reference list
-  | VernacImport of export_flag * reference list
-  | VernacCanonical of reference or_by_notation
-  | VernacCoercion of reference or_by_notation *
+      qualid option * export_flag option * qualid list
+  | VernacImport of export_flag * qualid list
+  | VernacCanonical of qualid or_by_notation
+  | VernacCoercion of qualid or_by_notation *
       class_rawexpr * class_rawexpr
   | VernacIdentityCoercion of lident * class_rawexpr * class_rawexpr
   | VernacNameSectionHypSet of lident * section_subset_expr
@@ -367,9 +367,9 @@ type nonrec vernac_expr =
   | VernacContext of local_binder_expr list
 
   | VernacDeclareInstances of
-    (reference * Hints.hint_info_expr) list (* instances names, priorities and patterns *)
+    (qualid * Hints.hint_info_expr) list (* instances names, priorities and patterns *)
 
-  | VernacDeclareClass of reference (* inductive or definition name *)
+  | VernacDeclareClass of qualid (* inductive or definition name *)
 
   (* Modules and Module Types *)
   | VernacDeclareModule of bool option * lident *
@@ -403,11 +403,11 @@ type nonrec vernac_expr =
 
   (* Commands *)
   | VernacCreateHintDb of string * bool
-  | VernacRemoveHints of string list * reference list
+  | VernacRemoveHints of string list * qualid list
   | VernacHints of string list * Hints.hints_expr
   | VernacSyntacticDefinition of lident * (Id.t list * constr_expr) *
       onlyparsing_flag
-  | VernacArguments of reference or_by_notation *
+  | VernacArguments of qualid or_by_notation *
       vernac_argument_status list (* Main arguments status list *) *
         (Name.t * vernac_implicit_status) list list (* Extra implicit status lists *) *
       int option (* Number of args to trigger reduction *) *
@@ -416,9 +416,9 @@ type nonrec vernac_expr =
           `DefaultImplicits ] list
   | VernacReserve of simple_binder list
   | VernacGeneralizable of (lident list) option
-  | VernacSetOpacity of (Conv_oracle.level * reference or_by_notation list)
+  | VernacSetOpacity of (Conv_oracle.level * qualid or_by_notation list)
   | VernacSetStrategy of
-      (Conv_oracle.level * reference or_by_notation list) list
+      (Conv_oracle.level * qualid or_by_notation list) list
   | VernacUnsetOption of export_flag * Goptions.option_name
   | VernacSetOption of export_flag * Goptions.option_name * option_value
   | VernacAddOption of Goptions.option_name * option_ref_value list