1 files changed, 2 insertions, 4 deletions
diff --git a/theories/FSets/FSetCompat.v b/theories/FSets/FSetCompat.v
index 971daa215..439f0e528 100644
--- a/theories/FSets/FSetCompat.v
+++ b/theories/FSets/FSetCompat.v
@@ -209,10 +209,8 @@ Module Backport_Sets
   Qed.
   Definition compare : forall s s', Compare lt eq s s'.
   Proof.
-   intros s s'.
-   assert (H := M.compare_spec s s').
-   destruct (M.compare s s'); [ apply EQ | apply LT | apply GT ];
-    inversion H; auto.
+   intros s s'; destruct (CompSpec2Type (M.compare_spec s s'));
+    [ apply EQ | apply LT | apply GT ]; auto.
   Defined.
 
 End Backport_Sets.