From ffe69a288e2fb4f03ce4c294def8ed727b666ce3 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 3 Mar 2016 14:31:58 +0100
Subject: [PATCH] Hint database for set_solver.

---
 prelude/collections.v | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/prelude/collections.v b/prelude/collections.v
index 1a36815db..08f391b49 100644
--- a/prelude/collections.v
+++ b/prelude/collections.v
@@ -265,6 +265,7 @@ Ltac set_unfold :=
 [set_solver] already. We use the [naive_solver] tactic as a substitute.
 This tactic either fails or proves the goal. *)
 Tactic Notation "set_solver" "by" tactic3(tac) :=
+  try done;
   intros; setoid_subst;
   set_unfold;
   intros; setoid_subst;
@@ -278,6 +279,10 @@ Tactic Notation "set_solver" := set_solver by idtac.
 Tactic Notation "set_solver" "-" hyp_list(Hs) := clear Hs; set_solver.
 Tactic Notation "set_solver" "+" hyp_list(Hs) := clear -Hs; set_solver.
 
+Hint Extern 1000 (_ ∉ _) => set_solver : set_solver.
+Hint Extern 1000 (_ ∈ _) => set_solver : set_solver.
+Hint Extern 1000 (_ ⊆ _) => set_solver : set_solver.
+
 (** * Conversion of option and list *)
 Definition of_option `{Singleton A C, Empty C} (mx : option A) : C :=
   match mx with None => ∅ | Some x => {[ x ]} end.
-- 
GitLab