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 605781993..e38da45b9 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 ce37c3614..bca419c9a 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 fe6cf73c7..5e5d00362 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 0375cfc92..8dd729610 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 72030dc9f..d76bd1e2b 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