From ba5e4a82b455d2239a606066ba71f950355cbb10 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 29 Oct 2020 09:19:34 +0100
Subject: [PATCH] fix build

---
 theories/sets.v | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/theories/sets.v b/theories/sets.v
index 8c8bfba0..14005f60 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. *)
-- 
GitLab