Skip to content
Snippets Groups Projects
Commit 02d397ed authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Remove useless import.

parent b6b4b694
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Showing
with 0 additions and 1 deletion
iris/base_logic/upred.v
+ 0
− 1
View file @ 02d397ed
From stdpp Require Import finite.
From iris.algebra Require Export cmra updates.
From iris.bi Require Import notation.
From iris.prelude Require Import options.
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment