Abstract the datatype of maps of hint modes.

This is the only datatype in the API that exposes a use to
the canonical-name-based GlobRef.Map.t type.

tactics/class_tactics.ml

@@ -466,7 +466,7 @@ module Search = struct
 
   (** Local hints *)
   let autogoal_cache = Summary.ref ~name:"autogoal_cache"
-      (DirPath.empty, true, Context.Named.empty, GlobRef.Map.empty,
+      (DirPath.empty, true, Context.Named.empty, Hints.Modes.empty,
        Hint_db.empty TransparentState.full true)
 
   let make_autogoal_hints only_classes (modes,st as mst) gl =
@@ -1090,7 +1090,7 @@ let typeclasses_eauto ?(only_classes=false)
   in
   let st = match dbs with x :: _ -> Hint_db.transparent_state x | _ -> st in
   let modes = List.map Hint_db.modes dbs in
-  let modes = List.fold_left (GlobRef.Map.union (fun _ m1 m2 -> Some (m1@m2))) GlobRef.Map.empty modes in
+  let modes = List.fold_left Modes.union Modes.empty modes in
   let depth = match depth with None -> get_typeclasses_depth () | Some l -> Some l in
   Proofview.tclIGNORE
     (Search.eauto_tac (modes,st) ~only_classes ?strategy

tactics/class_tactics.mli

@@ -86,7 +86,7 @@ val deactivate_solver : name:CString.Map.key -> unit
 
 module Search : sig
   val eauto_tac :
-    Hints.hint_mode array list GlobRef.Map.t * TransparentState.t
+    Hints.Modes.t * TransparentState.t
     (** The transparent_state and modes used when working with local hypotheses  *)
     -> ?unique:bool
     (** Should we force a unique solution *)

tactics/hints.ml

@@ -183,6 +183,13 @@ type hint_mode =
   | ModeNoHeadEvar (* No evar at the head *)
   | ModeOutput (* Anything *)
 
+module Modes =
+struct
+  type t = hint_mode array list GlobRef.Map.t
+  let empty = GlobRef.Map.empty
+  let union m1 m2 = GlobRef.Map.union (fun _ m1 m2 -> Some (m1@m2)) m1 m2
+end
+
 type 'a hints_transparency_target =
   | HintsVariables
   | HintsConstants

tactics/hints.mli

@@ -110,6 +110,13 @@ type 'a with_mode =
   | ModeMatch of mode_match * 'a
   | ModeMismatch
 
+module Modes :
+sig
+  type t
+  val empty : t
+  val union : t -> t -> t
+end
+
 module Hint_db :
   sig
     type t
@@ -150,8 +157,8 @@ module Hint_db :
 
     val unfolds : t -> Id.Set.t * Cset.t * PRset.t
 
-    val add_modes : hint_mode array list GlobRef.Map.t -> t -> t
-    val modes : t -> hint_mode array list GlobRef.Map.t
+    val add_modes : Modes.t -> t -> t
+    val modes : t -> Modes.t
   end
 
 type hint_db = Hint_db.t