diff --git a/FiniteSets/interfaces/lattice_examples.v b/FiniteSets/interfaces/lattice_examples.v
index 1eb26db..647f937 100644
--- a/FiniteSets/interfaces/lattice_examples.v
+++ b/FiniteSets/interfaces/lattice_examples.v
@@ -51,7 +51,7 @@ End BoolLattice.
 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 commutativity : bool_lattice_hints.
 Hint Resolve absorb : bool_lattice_hints.
 Hint Resolve idempotency : bool_lattice_hints.
 Hint Resolve neutralityL : bool_lattice_hints.
@@ -247,4 +247,4 @@ Section hPropLattice.
       absorption_min_max := _ ;
       absorption_max_min := _
   }.
-End hPropLattice.
\ No newline at end of file
+End hPropLattice.
diff --git a/FiniteSets/interfaces/lattice_interface.v b/FiniteSets/interfaces/lattice_interface.v
index 103daea..965aa2d 100644
--- a/FiniteSets/interfaces/lattice_interface.v
+++ b/FiniteSets/interfaces/lattice_interface.v
@@ -8,7 +8,7 @@ Section binary_operation.
            (f : operation A).
 
   Class Commutative :=
-    commutative : forall x y, f x y = f y x.
+    commutativity : forall x y, f x y = f y x.
 
   Class Associative :=
     associativity : forall x y z, f (f x y) z = f x (f y z).
@@ -36,7 +36,7 @@ Arguments Idempotent {_} _.
 Arguments NeutralL {_} _ _.
 Arguments NeutralR {_} _ _.
 Arguments Absorption {_} _ _.
-Arguments commutative {_} {_} {_} _ _.
+Arguments commutativity {_} {_} {_} _ _.
 Arguments associativity {_} {_} {_} _ _ _.
 Arguments idempotency {_} {_} {_} _.
 Arguments neutralityL {_} {_} {_} {_} _.
@@ -79,7 +79,7 @@ Arguments JoinSemiLattice _ {_} {_}.
 Create HintDb joinsemilattice_hints.
 Hint Resolve associativity : joinsemilattice_hints.
 Hint Resolve (associativity _ _ _)^ : joinsemilattice_hints.
-Hint Resolve commutative : joinsemilattice_hints.
+Hint Resolve commutativity : joinsemilattice_hints.
 Hint Resolve idempotency : joinsemilattice_hints.
 Hint Resolve neutralityL : joinsemilattice_hints.
 Hint Resolve neutralityR : joinsemilattice_hints.
@@ -108,8 +108,8 @@ Arguments Lattice _ {_} {_} {_}.
 Create HintDb lattice_hints.
 Hint Resolve associativity : lattice_hints.
 Hint Resolve (associativity _ _ _)^ : lattice_hints.
-Hint Resolve commutative : lattice_hints.
+Hint Resolve commutativity : lattice_hints.
 Hint Resolve absorb : lattice_hints.
 Hint Resolve idempotency : lattice_hints.
 Hint Resolve neutralityL : lattice_hints.
-Hint Resolve neutralityR : lattice_hints.
\ No newline at end of file
+Hint Resolve neutralityR : lattice_hints.
diff --git a/FiniteSets/subobjects/b_finite.v b/FiniteSets/subobjects/b_finite.v
index 1cb4154..e222025 100644
--- a/FiniteSets/subobjects/b_finite.v
+++ b/FiniteSets/subobjects/b_finite.v
@@ -428,7 +428,7 @@ Section kfin_bfin.
         apply path_forall. intro a.
         unfold union, sub_union, max_fun.
         rewrite HX.
-        rewrite (commutative (X' a)).
+        rewrite (commutativity (X' a)).
         rewrite (associativity _ (X' a)).
         apply path_iff_hprop.
         * intros Ha.