Remove reference name type.

reference was defined as Ident or Qualid, but the qualid type already
permits empty paths. So we had effectively two representations for
unqualified names, that were not seen as equal by eq_reference.

We remove the reference type and replace its uses by qualid.

5 files changed, 27 insertions, 30 deletions

diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
index 6057819931..e38da45b95 100644
--- a/printing/ppconstr.ml
+++ b/printing/ppconstr.ml
@@ -159,7 +159,7 @@ let tag_var = tag Tag.variable
 
   let pr_univ_expr = function
     | Some (x,n) ->
-       pr_reference x ++ (match n with 0 -> mt () | _ -> str"+" ++ int n)
+       pr_qualid x ++ (match n with 0 -> mt () | _ -> str"+" ++ int n)
     | None -> str"_"
 
   let pr_univ l =
@@ -180,7 +180,7 @@ let tag_var = tag Tag.variable
     | GSet -> tag_type (str "Set")
     | GType UUnknown -> tag_type (str "Type")
     | GType UAnonymous -> tag_type (str "_")
-    | GType (UNamed u) -> tag_type (pr_reference u)
+    | GType (UNamed u) -> tag_type (pr_qualid u)
 
   let pr_qualid sp =
     let (sl, id) = repr_qualid sp in
@@ -205,16 +205,16 @@ let tag_var = tag Tag.variable
       tag_type (str "Set")
     | GType u ->
       (match u with
-        | UNamed u -> pr_reference u
+        | UNamed u -> pr_qualid u
         | UAnonymous -> tag_type (str "Type")
         | UUnknown -> tag_type (str "_"))
 
   let pr_universe_instance l =
     pr_opt_no_spc (pr_univ_annot (prlist_with_sep spc pr_glob_sort_instance)) l
 
-  let pr_reference = CAst.with_val (function
-  | Qualid qid -> pr_qualid qid
-  | Ident id -> tag_var (pr_id id))
+  let pr_reference qid =
+    if qualid_is_ident qid then tag_var (pr_id @@ qualid_basename qid)
+    else pr_qualid qid
 
   let pr_cref ref us =
     pr_reference ref ++ pr_universe_instance us
@@ -564,9 +564,9 @@ let tag_var = tag Tag.variable
           return (p ++ prlist (pr spc (lapp,L)) l2, lapp)
         else
           return (p, lproj)
-      | CAppExpl ((None,{v=Ident var},us),[t])
-      | CApp ((_, {v = CRef({v=Ident var},us)}),[t,None])
-          when Id.equal var Notation_ops.ldots_var ->
+      | CAppExpl ((None,qid,us),[t])
+      | CApp ((_, {v = CRef(qid,us)}),[t,None])
+          when qualid_is_ident qid && Id.equal (qualid_basename qid) Notation_ops.ldots_var ->
         return (
           hov 0 (str ".." ++ pr spc (latom,E) t ++ spc () ++ str ".."),
           larg
diff --git a/printing/ppconstr.mli b/printing/ppconstr.mli
index ce37c3614a..bca419c9ac 100644
--- a/printing/ppconstr.mli
+++ b/printing/ppconstr.mli
@@ -47,7 +47,7 @@ val pr_guard_annot : (constr_expr -> Pp.t) ->
   lident option * recursion_order_expr ->
   Pp.t
 
-val pr_record_body : (reference * constr_expr) list -> Pp.t
+val pr_record_body : (qualid * constr_expr) list -> Pp.t
 val pr_binders : local_binder_expr list -> Pp.t
 val pr_constr_pattern_expr : constr_pattern_expr -> Pp.t
 val pr_lconstr_pattern_expr : constr_pattern_expr -> Pp.t
diff --git a/printing/prettyp.ml b/printing/prettyp.ml
index fe6cf73c79..5e5d003622 100644
--- a/printing/prettyp.ml
+++ b/printing/prettyp.ml
@@ -344,8 +344,7 @@ let register_locatable name f =
 
 exception ObjFound of logical_name
 
-let locate_any_name ref =
-  let {v=qid} = qualid_of_reference ref in
+let locate_any_name qid =
   try Term (Nametab.locate qid)
   with Not_found ->
   try Syntactic (Nametab.locate_syndef qid)
@@ -452,8 +451,7 @@ type locatable_kind =
 | LocOther of string
 | LocAny
 
-let print_located_qualid name flags ref =
-  let {v=qid} = qualid_of_reference ref in
+let print_located_qualid name flags qid =
   let located = match flags with
   | LocTerm -> locate_term qid
   | LocModule -> locate_modtype qid @ locate_module qid
@@ -787,10 +785,9 @@ let print_full_pure_context env sigma =
    follows the definition of the inductive type *)
 
 (* This is designed to print the contents of an opened section *)
-let read_sec_context r =
-  let qid = qualid_of_reference r in
+let read_sec_context qid =
   let dir =
-    try Nametab.locate_section qid.v
+    try Nametab.locate_section qid
     with Not_found ->
       user_err ?loc:qid.loc ~hdr:"read_sec_context" (str "Unknown section.") in
   let rec get_cxt in_cxt = function
diff --git a/printing/prettyp.mli b/printing/prettyp.mli
index 0375cfc921..8dd7296100 100644
--- a/printing/prettyp.mli
+++ b/printing/prettyp.mli
@@ -24,20 +24,20 @@ val print_library_entry : env -> Evd.evar_map -> bool -> (object_name * Lib.node
 val print_full_context : env -> Evd.evar_map -> Pp.t
 val print_full_context_typ : env -> Evd.evar_map -> Pp.t
 val print_full_pure_context : env -> Evd.evar_map -> Pp.t
-val print_sec_context : env -> Evd.evar_map -> reference -> Pp.t
-val print_sec_context_typ : env -> Evd.evar_map -> reference -> Pp.t
+val print_sec_context : env -> Evd.evar_map -> qualid -> Pp.t
+val print_sec_context_typ : env -> Evd.evar_map -> qualid -> Pp.t
 val print_judgment : env -> Evd.evar_map -> EConstr.unsafe_judgment -> Pp.t
 val print_safe_judgment : env -> Evd.evar_map -> Safe_typing.judgment -> Pp.t
 val print_eval :
   reduction_function -> env -> Evd.evar_map ->
     Constrexpr.constr_expr -> EConstr.unsafe_judgment -> Pp.t
 
-val print_name : env -> Evd.evar_map -> reference Constrexpr.or_by_notation ->
+val print_name : env -> Evd.evar_map -> qualid Constrexpr.or_by_notation ->
   UnivNames.univ_name_list option -> Pp.t
-val print_opaque_name : env -> Evd.evar_map -> reference -> Pp.t
-val print_about : env -> Evd.evar_map -> reference Constrexpr.or_by_notation ->
+val print_opaque_name : env -> Evd.evar_map -> qualid -> Pp.t
+val print_about : env -> Evd.evar_map -> qualid Constrexpr.or_by_notation ->
   UnivNames.univ_name_list option -> Pp.t
-val print_impargs : reference Constrexpr.or_by_notation -> Pp.t
+val print_impargs : qualid Constrexpr.or_by_notation -> Pp.t
 
 (** Pretty-printing functions for classes and coercions *)
 val print_graph : env -> evar_map -> Pp.t
@@ -77,10 +77,10 @@ val register_locatable : string -> 'a locatable_info -> unit
     name describing the kind of objects considered and that is added as a
     grammar command prefix for vernacular commands Locate. *)
 
-val print_located_qualid : reference -> Pp.t
-val print_located_term : reference -> Pp.t
-val print_located_module : reference -> Pp.t
-val print_located_other : string -> reference -> Pp.t
+val print_located_qualid : qualid -> Pp.t
+val print_located_term : qualid -> Pp.t
+val print_located_module : qualid -> Pp.t
+val print_located_other : string -> qualid -> Pp.t
 
 type object_pr = {
   print_inductive           : MutInd.t -> UnivNames.univ_name_list option -> Pp.t;
diff --git a/printing/printer.ml b/printing/printer.ml
index 72030dc9f6..d76bd1e2b2 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -229,15 +229,15 @@ let dirpath_of_global = function
     dirpath_of_mp (MutInd.modpath kn)
   | VarRef _ -> DirPath.empty
 
-let qualid_of_global env r =
-  Libnames.make_qualid (dirpath_of_global r) (id_of_global env r)
+let qualid_of_global ?loc env r =
+  Libnames.make_qualid ?loc (dirpath_of_global r) (id_of_global env r)
 
 let safe_gen f env sigma c =
   let orig_extern_ref = Constrextern.get_extern_reference () in
   let extern_ref ?loc vars r =
     try orig_extern_ref vars r
     with e when CErrors.noncritical e ->
-      CAst.make ?loc @@ Libnames.Qualid (qualid_of_global env r)
+      qualid_of_global ?loc env r
   in
   Constrextern.set_extern_reference extern_ref;
   try