Remove unused nametab for qvars

It might have been useful if we had section level qvars but currently
is unused.

We keep this commit instead of squashing into the commit which
introduced this nametab so that if we ever want section level qvars we
can revert or otherwise use it as a basis.

engine/uState.ml

@@ -745,7 +745,7 @@ let id_of_qvar uctx l =
 let qualid_of_qvar_names (bind, (qrev,_)) l =
   try Some (Libnames.qualid_of_ident (Option.get (QVar.Map.find l qrev).uname))
   with Not_found | Option.IsNone ->
-    UnivNames.qualid_of_qvar bind l
+    None (* no global qvars *)
 
 let qualid_of_level_names (bind, (_,urev)) l =
   try Some (Libnames.qualid_of_ident (Option.get (Level.Map.find l urev).uname))

engine/univNames.ml

@@ -35,12 +35,3 @@ let pr_level_with_global_universes ?(binders=empty_binders) l =
   match qualid_of_level binders l with
   | Some qid  -> Libnames.pr_qualid qid
   | None -> Level.raw_pr l
-
-let qualid_of_qvar (ctx,_) l =
-  try Some (Nametab.shortest_qualid_of_qvar ctx l)
-  with Not_found -> None
-
-let pr_qvar_with_global_universes ?(binders=empty_binders) l =
-  match qualid_of_qvar binders l with
-  | Some qid  -> Libnames.pr_qualid qid
-  | None -> QVar.raw_pr l

engine/univNames.mli

@@ -28,6 +28,3 @@ type full_name_list = lname list * lname list
 
 val pr_level_with_global_universes : ?binders:universe_binders -> Level.t -> Pp.t
 val qualid_of_level : universe_binders -> Level.t -> Libnames.qualid option
-
-val pr_qvar_with_global_universes : ?binders:universe_binders -> QVar.t -> Pp.t
-val qualid_of_qvar : universe_binders -> QVar.t -> Libnames.qualid option

interp/constrextern.ml

@@ -859,10 +859,7 @@ let extern_glob_qvar uvars = function
   | GLocalQVar {v=Anonymous;loc} -> CQAnon loc
   | GLocalQVar {v=Name id; loc} -> CQVar (qualid_of_ident ?loc id)
   | GRawQVar q -> CRawQVar q
-  | GQVar q -> begin match UnivNames.qualid_of_qvar uvars q with
-      | Some qid -> CQVar qid
-      | None -> CRawQVar q
-    end
+  | GQVar q -> CRawQVar q
 
 let extern_glob_quality uvars = function
   | GQConstant q -> CQConstant q

interp/constrintern.ml

@@ -1210,12 +1210,10 @@ let intern_qvar ~local_univs = function
     match local with
     | Some u -> GQVar u
     | None ->
-      try GQVar (Nametab.locate_qvar qid)
-      with Not_found ->
-        if is_id && local_univs.unb_univs
-        then GLocalQVar (CAst.make ?loc:qid.loc (Name (qualid_basename qid)))
-        else
-          CErrors.user_err ?loc:qid.loc Pp.(str "Undeclared quality " ++ pr_qualid qid ++ str".")
+      if is_id && local_univs.unb_univs
+      then GLocalQVar (CAst.make ?loc:qid.loc (Name (qualid_basename qid)))
+      else
+        CErrors.user_err ?loc:qid.loc Pp.(str "Undeclared quality " ++ pr_qualid qid ++ str".")
 
 let intern_quality ~local_univs q =
   match q with

kernel/sorts.mli

@@ -29,6 +29,8 @@ sig
   val hash : t -> int
 
   val raw_pr : t -> Pp.t
+  (** Using this is incorrect when names are available, typically from an evar map. *)
+
   val to_string : t -> string
   (** Debug printing *)
 

library/nametab.ml

@@ -386,10 +386,6 @@ module UnivTab = Make(FullPath)(Univ.UGlobal)
 type univtab = UnivTab.t
 let the_univtab = Summary.ref ~name:"univtab" (UnivTab.empty : univtab)
 
-module QVarTab = Make(FullPath)(Sorts.QVar)
-type qvartab = QVarTab.t
-let the_qvartab = Summary.ref ~name:"qvartab" (QVarTab.empty : qvartab)
-
 (* Reversed name tables ***************************************************)
 
 (* This table translates extended_global_references back to section paths *)
@@ -408,11 +404,6 @@ module UnivIdMap = HMap.Make(Univ.UGlobal)
 type univrevtab = full_path UnivIdMap.t
 let the_univrevtab = Summary.ref ~name:"univrevtab" (UnivIdMap.empty : univrevtab)
 
-module QVarIdMap = HMap.Make(Sorts.QVar)
-
-type qvarrevtab = full_path QVarIdMap.t
-let the_qvarrevtab = Summary.ref ~name:"qvarrevtab" (QVarIdMap.empty : qvarrevtab)
-
 (** Module-related nametab *)
 module Modules = struct
 
@@ -503,11 +494,6 @@ let push_universe vis sp univ =
   the_univtab := UnivTab.push vis sp univ !the_univtab;
   the_univrevtab := UnivIdMap.add univ sp !the_univrevtab
 
-let push_qvar vis sp q =
-  assert (Option.is_empty (Sorts.QVar.var_index q));
-  the_qvartab := QVarTab.push vis sp q !the_qvartab;
-  the_qvarrevtab := QVarIdMap.add q sp !the_qvarrevtab
-
 (* Reverse locate functions ***********************************************)
 
 let path_of_global ref =
@@ -534,9 +520,6 @@ let path_of_modtype mp =
 let path_of_universe mp =
   UnivIdMap.find mp !the_univrevtab
 
-let path_of_qvar mp =
-  QVarIdMap.find mp !the_qvarrevtab
-
 (* Shortest qualid functions **********************************************)
 
 let shortest_qualid_of_global ?loc ctx ref =
@@ -563,10 +546,6 @@ let shortest_qualid_of_universe ?loc ctx kn =
   let sp = UnivIdMap.find kn !the_univrevtab in
   UnivTab.shortest_qualid_gen ?loc (fun id -> Id.Map.mem id ctx) sp !the_univtab
 
-let shortest_qualid_of_qvar ?loc ctx kn =
-  let sp = QVarIdMap.find kn !the_qvarrevtab in
-  QVarTab.shortest_qualid_gen ?loc (fun id -> Id.Map.mem id ctx) sp !the_qvartab
-
 let pr_global_env env ref =
   try pr_qualid (shortest_qualid_of_global env ref)
   with Not_found as exn ->
@@ -630,8 +609,6 @@ let full_name_modtype qid = MPTab.user_name qid Modules.(!nametab.modtypetab)
 
 let locate_universe qid = UnivTab.locate qid !the_univtab
 
-let locate_qvar qid = QVarTab.locate qid !the_qvartab
-
 let locate_dir qid = DirTab.locate qid Modules.(!nametab.dirtab)
 
 let locate_module qid = MPDTab.locate qid Modules.(!nametab.modtab)
@@ -708,5 +685,3 @@ let exists_module dir = MPDTab.exists dir Modules.(!nametab.modtab)
 let exists_modtype sp = MPTab.exists sp Modules.(!nametab.modtypetab)
 
 let exists_universe kn = UnivTab.exists kn !the_univtab
-
-let exists_qvar kn = QVarTab.exists kn !the_qvartab

library/nametab.mli

@@ -112,8 +112,6 @@ val push_abbreviation : ?deprecated:Deprecation.t -> visibility -> full_path ->
 
 val push_universe : visibility -> full_path -> Univ.UGlobal.t -> unit
 
-val push_qvar : visibility -> full_path -> Sorts.QVar.t -> unit
-
 (** Deprecation info *)
 
 val is_deprecated_xref : Globnames.extended_global_reference -> Deprecation.t option
@@ -134,7 +132,6 @@ val locate_dir : qualid -> GlobDirRef.t
 val locate_module : qualid -> ModPath.t
 val locate_section : qualid -> DirPath.t
 val locate_universe : qualid -> Univ.UGlobal.t
-val locate_qvar : qualid -> Sorts.QVar.t
 
 val locate_extended_nowarn : qualid -> Globnames.extended_global_reference * Deprecation.t option
 
@@ -176,7 +173,6 @@ val exists_modtype : full_path -> bool
 val exists_module : DirPath.t -> bool
 val exists_dir : DirPath.t -> bool
 val exists_universe : full_path -> bool
-val exists_qvar : full_path -> bool
 
 (** {6 These functions locate qualids into full user names } *)
 
@@ -199,8 +195,6 @@ val path_of_modtype : ModPath.t -> full_path
     @raise Not_found if the universe was not introduced by the user. *)
 val path_of_universe : Univ.UGlobal.t -> full_path
 
-val path_of_qvar : Sorts.QVar.t -> full_path
-
 (** Returns in particular the dirpath or the basename of the full path
    associated to global reference *)
 
@@ -225,8 +219,6 @@ val shortest_qualid_of_module : ?loc:Loc.t -> ModPath.t -> qualid
 (** In general we have a [UnivNames.universe_binders] around rather than a [Id.Set.t] *)
 val shortest_qualid_of_universe : ?loc:Loc.t -> 'u Id.Map.t -> Univ.UGlobal.t -> qualid
 
-val shortest_qualid_of_qvar : ?loc:Loc.t -> 'u Id.Map.t -> Sorts.QVar.t -> qualid
-
 (** {5 Generic name handling} *)
 
 (** NOT FOR PUBLIC USE YET. Plugin writers, please do not rely on this API. *)

vernac/himsg.ml

@@ -1086,7 +1086,7 @@ let explain_not_match_error = function
   | IncompatibleUniverses incon ->
     str"the universe constraints are inconsistent: " ++
     UGraph.explain_universe_inconsistency
-      UnivNames.pr_qvar_with_global_universes
+      Sorts.QVar.raw_pr
       UnivNames.pr_level_with_global_universes
       incon
   | IncompatiblePolymorphism (env, t1, t2) ->
@@ -1550,7 +1550,7 @@ let rec vernac_interp_error_handler = function
   | UGraph.UniverseInconsistency i ->
     str "Universe inconsistency." ++ spc() ++
     UGraph.explain_universe_inconsistency
-      UnivNames.pr_qvar_with_global_universes
+      Sorts.QVar.raw_pr
       UnivNames.pr_level_with_global_universes
       i ++ str "."
   | TypeError(env,te) ->