diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index 966c44e9cc4b51188ea3637b52597210c1f822c5..9209cecb268e77e2ab4e362fee28f01a91de98bf 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -2184,7 +2184,7 @@ Ltac decompose_map_disjoint := repeat
 
 (** To prove a disjointness property, we first decompose all hypotheses, and
 then use an auto database to prove the required property. *)
-Create HintDb map_disjoint.
+Create HintDb map_disjoint discriminated.
 Ltac solve_map_disjoint :=
   solve [decompose_map_disjoint; auto with map_disjoint].
 
@@ -2258,7 +2258,7 @@ Tactic Notation "simpl_map" "by" tactic3(tac) := repeat
     rewrite E; clear E
   end.
 
-Create HintDb simpl_map.
+Create HintDb simpl_map discriminated.
 Tactic Notation "simpl_map" := simpl_map by eauto with simpl_map map_disjoint.
 
 Hint Extern 80 ((_ ∪ _) !! _ = Some _) => apply lookup_union_Some_l : simpl_map.
diff --git a/theories/namespaces.v b/theories/namespaces.v
index 9bd02fcd809864c74bb1f44d026af45e4d0a4bd1..12dc464c30dcb6ed410c8d9c228d4673d9fc2ef7 100644
--- a/theories/namespaces.v
+++ b/theories/namespaces.v
@@ -73,7 +73,7 @@ of the forms:
 - [N1 ## N2]
 - [↑N1 ⊆ E ∖ ↑N2 ∖ .. ∖ ↑Nn]
 - [E1 ∖ ↑N1 ⊆ E2 ∖ ↑N2 ∖ .. ∖ ↑Nn] *)
-Create HintDb ndisj.
+Create HintDb ndisj discriminated.
 
 (** Rules for goals of the form [_ ⊆ _] *)
 (** If-and-only-if rules. Well, not quite, but for the fragment we are