From 5ee7053631a7495168fb37de8ae2326c8873c7b3 Mon Sep 17 00:00:00 2001
From: Niels <nnmvdw@gmail.com>
Date: Tue, 1 Aug 2017 17:35:23 +0200
Subject: [PATCH] Removed bad hints

---
 FiniteSets/disjunction.v      | 11 ++---------
 FiniteSets/fsets/operations.v |  6 +++---
 2 files changed, 5 insertions(+), 12 deletions(-)

diff --git a/FiniteSets/disjunction.v b/FiniteSets/disjunction.v
index d198ace..fe8c1dd 100644
--- a/FiniteSets/disjunction.v
+++ b/FiniteSets/disjunction.v
@@ -84,7 +84,7 @@ Open Scope logic_scope.
 Section hPropLattice.
   Context `{Univalence}.
 
-  Instance lor_commutative : Commutative lor.
+  Global Instance lor_commutative : Commutative lor.
   Proof.
     unfold Commutative.
     intros.
@@ -182,11 +182,4 @@ Section hPropLattice.
       absorption_max_min := _
   }.
   
-End hPropLattice.
-
-Hint Resolve
-     commutative_min commutative_max associative_min associative_max
-     idempotent_min idempotent_max
-     neutralL_min neutralR_min
-     absorption_min_max absorption_max_min
- : lattice_hints.
\ No newline at end of file
+End hPropLattice.
\ No newline at end of file
diff --git a/FiniteSets/fsets/operations.v b/FiniteSets/fsets/operations.v
index 81c6bf0..0da4ff9 100644
--- a/FiniteSets/fsets/operations.v
+++ b/FiniteSets/fsets/operations.v
@@ -17,9 +17,9 @@ hrecursion.
   exact _.
 - apply lor.
 - intros ; symmetry ; apply lor_assoc.
-- intros ; apply lor_comm.
-- intros ; apply lor_nl.
-- intros ; apply lor_nr.
+- apply lor_commutative.
+- apply lor_nl.
+- apply lor_nr.
 - intros ; apply lor_idem.
 Defined.