From 02d397ed2df5a465ee099cc3bcf4540f25aaead2 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 12 Aug 2022 13:28:18 +0200
Subject: [PATCH] Remove useless import.

---
 iris/base_logic/upred.v | 1 -
 1 file changed, 1 deletion(-)

diff --git a/iris/base_logic/upred.v b/iris/base_logic/upred.v
index 749685bb2..8fe8c536f 100644
--- a/iris/base_logic/upred.v
+++ b/iris/base_logic/upred.v
@@ -1,4 +1,3 @@
-From stdpp Require Import finite.
 From iris.algebra Require Export cmra updates.
 From iris.bi Require Import notation.
 From iris.prelude Require Import options.
-- 
GitLab