Remove dead code in Globnames.

5 files changed, 3 insertions, 23 deletions

diff --git a/engine/univGen.ml b/engine/univGen.ml
index 1fe09270ba..b270f9dc0b 100644
--- a/engine/univGen.ml
+++ b/engine/univGen.ml
@@ -48,8 +48,6 @@ let fresh_instance_from ?loc ctx = function
 
 (** Fresh universe polymorphic construction *)
 
-open Globnames
-
 let fresh_global_instance ?loc ?names env gr =
   let auctx = Environ.universes_of_global env gr in
   let u, ctx = fresh_instance_from ?loc auctx names in
@@ -78,10 +76,6 @@ let constr_of_monomorphic_global gr =
       Pp.(str "globalization of polymorphic reference " ++ Nametab.pr_global_env Id.Set.empty gr ++
           str " would forget universes.")
 
-let fresh_global_or_constr_instance env = function
-  | IsConstr c -> c, ContextSet.empty
-  | IsGlobal gr -> fresh_global_instance env gr
-
 let fresh_sort_in_family = function
   | InSProp -> Sorts.sprop, ContextSet.empty
   | InProp -> Sorts.prop, ContextSet.empty
diff --git a/engine/univGen.mli b/engine/univGen.mli
index 1b351c61c4..bbde9d4e30 100644
--- a/engine/univGen.mli
+++ b/engine/univGen.mli
@@ -46,9 +46,6 @@ val fresh_constructor_instance : env -> constructor ->
 val fresh_global_instance : ?loc:Loc.t -> ?names:Univ.Instance.t -> env -> GlobRef.t ->
   constr in_universe_context_set
 
-val fresh_global_or_constr_instance : env -> Globnames.global_reference_or_constr ->
-  constr in_universe_context_set
-
 (** Get fresh variables for the universe context.
     Useful to make tactics that manipulate constrs in universe contexts polymorphic. *)
 val fresh_universe_context_set_instance : ContextSet.t ->
diff --git a/library/globnames.ml b/library/globnames.ml
index acb05f9ac0..63cb2c69bd 100644
--- a/library/globnames.ml
+++ b/library/globnames.ml
@@ -123,7 +123,3 @@ module ExtRefOrdered = struct
   | SynDef kn -> combinesmall 2 (KerName.hash kn)
 
 end
-
-type global_reference_or_constr =
-  | IsGlobal of GlobRef.t
-  | IsConstr of constr
diff --git a/library/globnames.mli b/library/globnames.mli
index 48cbb11b66..d61cdd2b64 100644
--- a/library/globnames.mli
+++ b/library/globnames.mli
@@ -59,7 +59,3 @@ module ExtRefOrdered : sig
   val equal : t -> t -> bool
   val hash : t -> int
 end
-
-type global_reference_or_constr =
-  | IsGlobal of GlobRef.t
-  | IsConstr of constr
diff --git a/vernac/classes.ml b/vernac/classes.ml
index c9b5144299..77bc4e4f8a 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -42,13 +42,10 @@ let () =
   Hook.set Typeclasses.classes_transparent_state_hook classes_transparent_state
 
 let add_instance_hint inst path local info poly =
-     let inst' = match inst with IsConstr c -> Hints.IsConstr (EConstr.of_constr c, Univ.ContextSet.empty)
-       | IsGlobal gr -> Hints.IsGlobRef gr
-     in
      Flags.silently (fun () ->
        Hints.add_hints ~local [typeclasses_db]
           (Hints.HintsResolveEntry
-             [info, poly, false, Hints.PathHints path, inst'])) ()
+             [info, poly, false, Hints.PathHints path, inst])) ()
 
 let is_local_for_hint i =
   match i.is_global with
@@ -61,9 +58,9 @@ let is_local_for_hint i =
 let add_instance check inst =
   let poly = Global.is_polymorphic inst.is_impl in
   let local = is_local_for_hint inst in
-  add_instance_hint (IsGlobal inst.is_impl) [inst.is_impl] local
+  add_instance_hint (Hints.IsGlobRef inst.is_impl) [inst.is_impl] local
     inst.is_info poly;
-  List.iter (fun (path, pri, c) -> add_instance_hint (IsConstr c) path
+  List.iter (fun (path, pri, c) -> add_instance_hint (Hints.IsConstr (EConstr.of_constr c, Univ.ContextSet.empty)) path
                 local pri poly)
     (build_subclasses ~check:(check && not (isVarRef inst.is_impl))
        (Global.env ()) (Evd.from_env (Global.env ())) inst.is_impl inst.is_info)