diff --git a/proofmode/tactics.v b/proofmode/tactics.v
index 72dacaf195a30b8384ee4c076af6fcd10d089a5a..a3de35f17cfe8afb1edcab027762cab910c29cd1 100644
--- a/proofmode/tactics.v
+++ b/proofmode/tactics.v
@@ -1,6 +1,6 @@
 From iris.proofmode Require Import coq_tactics intro_patterns spec_patterns.
 From iris.algebra Require Export upred.
-From iris.proofmode Require Export notation classes.
+From iris.proofmode Require Export classes notation.
 From iris.prelude Require Import stringmap hlist.
 
 Declare Reduction env_cbv := cbv [
diff --git a/tests/proofmode.v b/tests/proofmode.v
index 6b7697cb89f6f6832a34fbc803dbe4484b9e9130..67eee7e4d9fe07540ddda92db0b872aa46ffca9d 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -1,4 +1,4 @@
-From iris.proofmode Require Import tactics notation.
+From iris.proofmode Require Import tactics.
 From iris.proofmode Require Import pviewshifts invariants.
 
 Lemma demo_0 {M : ucmraT} (P Q : uPred M) :