diff --git a/theories/sets.v b/theories/sets.v
index 8c8bfba030255e19575eeeaa0d48674d799b6eef..14005f60e1ce9c04d88ff50d072c2927a6e1a30c 100644
--- a/theories/sets.v
+++ b/theories/sets.v
@@ -2,7 +2,8 @@
 importantly, it implements some tactics to automatically solve goals involving
 sets. *)
 From stdpp Require Export orders list list_numbers.
-From stdpp Require Import options finite.
+From stdpp Require Import finite.
+From stdpp Require Import options.
 
 (* FIXME: This file needs a 'Proof Using' hint, but they need to be set
 locally (or things moved out of sections) as no default works well enough. *)