From 29f3f31cec4b72ff8628e03c74f21b8497b40128 Mon Sep 17 00:00:00 2001
From: Niels <nnmvdw@gmail.com>
Date: Fri, 18 Aug 2017 11:18:37 +0200
Subject: [PATCH] Improved lattice hints

---
 FiniteSets/fsets/operations.v | 1 -
 FiniteSets/lattice.v          | 3 +++
 2 files changed, 3 insertions(+), 1 deletion(-)

diff --git a/FiniteSets/fsets/operations.v b/FiniteSets/fsets/operations.v
index 6484e78..034fe0d 100644
--- a/FiniteSets/fsets/operations.v
+++ b/FiniteSets/fsets/operations.v
@@ -45,7 +45,6 @@ Section operations.
   Proof.
     simple refine (FSet_rec _ _ _ true (fun _ => false) andb _ _ _ _ _)
     ; try eauto with bool_lattice_hints typeclass_instances.
-    intros ; symmetry ; eauto with lattice_hints typeclass_instances.
   Defined.
 
   Definition single_product {A B : Type} (a : A) : FSet B -> FSet (A * B).
diff --git a/FiniteSets/lattice.v b/FiniteSets/lattice.v
index fe55e25..97358eb 100644
--- a/FiniteSets/lattice.v
+++ b/FiniteSets/lattice.v
@@ -37,6 +37,7 @@ Arguments JoinSemiLattice _ {_} {_}.
 
 Create HintDb joinsemilattice_hints.
 Hint Resolve associativity : joinsemilattice_hints.
+Hint Resolve (associativity _ _ _)^ : joinsemilattice_hints.
 Hint Resolve commutative : joinsemilattice_hints.
 Hint Resolve idempotency : joinsemilattice_hints.
 Hint Resolve neutralityL : joinsemilattice_hints.
@@ -65,6 +66,7 @@ Arguments Lattice _ {_} {_} {_}.
 
 Create HintDb lattice_hints.
 Hint Resolve associativity : lattice_hints.
+Hint Resolve (associativity _ _ _)^ : lattice_hints.
 Hint Resolve commutative : lattice_hints.
 Hint Resolve absorb : lattice_hints.
 Hint Resolve idempotency : lattice_hints.
@@ -189,6 +191,7 @@ End sub_lattice.
 
 Create HintDb bool_lattice_hints.
 Hint Resolve associativity : bool_lattice_hints.
+Hint Resolve (associativity _ _ _)^ : bool_lattice_hints.
 Hint Resolve commutative : bool_lattice_hints.
 Hint Resolve absorb : bool_lattice_hints.
 Hint Resolve idempotency : bool_lattice_hints.