From 89eda68e5e9d7a12b10e3e72efe3e5f82381f8a2 Mon Sep 17 00:00:00 2001
From: Michael Sammler <noreply@sammler.me>
Date: Mon, 20 Apr 2020 09:11:41 +0200
Subject: [PATCH] Create HintDBs with the discriminated option

According to the documentation
https://coq.inria.fr/distrib/current/refman/proof-engine/tactics.html#coq:cmd.create-hintdb,
when creating a hint database without discrimination, Coq uses the
legacy implementation, which only uses Discrimination Trees for goals
without evars and does not use opaqueness information. This commit
switches the hint databases of stdpp to the new implementation.
---
 theories/fin_maps.v   | 4 ++--
 theories/namespaces.v | 2 +-
 2 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index 966c44e9..9209cecb 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 9bd02fcd..12dc464c 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
-- 
GitLab