From 9ae32c56abdf939e9b730580b12efb68cf78a6ca Mon Sep 17 00:00:00 2001
From: Guillaume Allais <guillaume.allais@ens-lyon.org>
Date: Tue, 16 Apr 2024 14:02:10 +0100
Subject: [PATCH] [ fix ] my silly mistake

---
 src/IO/Primitive.agda | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/IO/Primitive.agda b/src/IO/Primitive.agda
index 35460e2a36..324a32b643 100644
--- a/src/IO/Primitive.agda
+++ b/src/IO/Primitive.agda
@@ -8,7 +8,7 @@
 
 module IO.Primitive where
 
-open import IO.Primitive public
+open import IO.Primitive.Core public
 
 {-# WARNING_ON_IMPORT
 "IO.Primitive was deprecated in v2.1. Use IO.Primitive.Core instead."