diff --git a/theories/aneris_lang/lib/assert.v b/theories/aneris_lang/lib/assert.v
index a5c6ad5813e8d22173522e94211be8b9e3857812..bb51367a50812680adc54f23ad1297450674a293 100644
--- a/theories/aneris_lang/lib/assert.v
+++ b/theories/aneris_lang/lib/assert.v
@@ -1,6 +1,6 @@
 From iris.program_logic Require Export weakestpre.
 From iris.proofmode Require Import tactics.
-From aneris Require Import lang lifting tactics proofmode notation.
+From aneris.aneris_lang Require Import lang lifting tactics proofmode notation.
 
 Section code.
 
diff --git a/theories/aneris_lang/lib/bag.v b/theories/aneris_lang/lib/bag.v
index 39ae9ddff9b46771e3c453d9ee2bbbdce8c54e72..dc2116ec07f20eac11db58cb1db7e38e6025ebf4 100644
--- a/theories/aneris_lang/lib/bag.v
+++ b/theories/aneris_lang/lib/bag.v
@@ -3,7 +3,7 @@ From iris.algebra Require Import excl.
 From iris.base_logic.lib Require Export invariants.
 From iris.program_logic Require Export weakestpre.
 From iris.proofmode Require Import coq_tactics reduction.
-From aneris Require Import lang lifting tactics proofmode notation.
+From aneris.aneris_lang Require Import lang lifting tactics proofmode notation.
 From aneris.aneris_lang.lib Require Import lock.
 
 Definition newbag : ground_lang.val :=
diff --git a/theories/aneris_lang/lib/dictionary.v b/theories/aneris_lang/lib/dictionary.v
index bcccbaa6c954a46d97ee5675c86b71d47f36a650..618a6cfa5f8f466069eacfc020868327314cf6dc 100644
--- a/theories/aneris_lang/lib/dictionary.v
+++ b/theories/aneris_lang/lib/dictionary.v
@@ -1,6 +1,6 @@
 From stdpp Require Export strings list pretty gmap.
 From iris.proofmode Require Import tactics.
-From aneris Require Import lang network notation tactics proofmode lifting.
+From aneris.aneris_lang Require Import lang network notation tactics proofmode lifting.
 From aneris.aneris_lang.lib Require Import list.
 
 Module dict.
diff --git a/theories/aneris_lang/lib/lock.v b/theories/aneris_lang/lib/lock.v
index 25720172da5d1d7ab185b3742840f4e2fa07f924..9c0bca053365c3ccd6123de1d577609a0de6539c 100644
--- a/theories/aneris_lang/lib/lock.v
+++ b/theories/aneris_lang/lib/lock.v
@@ -3,7 +3,7 @@ From iris.algebra Require Import excl.
 From iris.base_logic.lib Require Export invariants.
 From iris.program_logic Require Export weakestpre.
 From iris.proofmode Require Import coq_tactics reduction.
-From aneris Require Import lang lifting tactics proofmode notation.
+From aneris.aneris_lang Require Import lang lifting tactics proofmode notation.
 
 Definition newlock : ground_lang.val := λ: <>, ref #false.
 Definition try_acquire : ground_lang.val := λ: "l", CAS "l" #false #true.
diff --git a/theories/aneris_lang/lib/network_helpers.v b/theories/aneris_lang/lib/network_helpers.v
index 20e2e3f3f4593acc73f005c63090db0d31ac9acf..855d519fd07027edb53cf3691da71a15c3176eef 100644
--- a/theories/aneris_lang/lib/network_helpers.v
+++ b/theories/aneris_lang/lib/network_helpers.v
@@ -1,6 +1,6 @@
 From iris.program_logic Require Export weakestpre.
 From iris.proofmode Require Import tactics.
-From aneris Require Import lang lifting tactics proofmode notation.
+From aneris.aneris_lang Require Import lang lifting tactics proofmode notation.
 From aneris.aneris_lang.lib Require Import assert.
 
 Section code.
diff --git a/theories/aneris_lang/lib/nodepar.v b/theories/aneris_lang/lib/nodepar.v
index ecbf4e74bf40cf79ad7046f41d908064eb50d779..638f6c997ccfdf29d6fc8ea79370ded05b701261 100644
--- a/theories/aneris_lang/lib/nodepar.v
+++ b/theories/aneris_lang/lib/nodepar.v
@@ -1,7 +1,7 @@
 From iris.base_logic.lib Require Export invariants.
 From iris.proofmode Require Import tactics.
 From iris.algebra Require Import excl.
-From aneris Require Export lang lifting network notation tactics proofmode.
+From aneris.aneris_lang Require Export lang lifting network notation tactics proofmode.
 Set Default Proof Using "Type".
 
 Notation "( n1 ; ip1 ; e1 ) ||| ( n2 ; ip2 ; e2 )" :=
diff --git a/theories/aneris_lang/lib/serialization/serialization_base.v b/theories/aneris_lang/lib/serialization/serialization_base.v
index ee9eb53231a0d0eb0950182222146445a4c83955..48065e0eb924335768be30d9e5512c2e325949fe 100644
--- a/theories/aneris_lang/lib/serialization/serialization_base.v
+++ b/theories/aneris_lang/lib/serialization/serialization_base.v
@@ -1,7 +1,7 @@
 From stdpp Require Import base pretty.
 From iris.program_logic Require Export weakestpre.
 From iris.proofmode Require Import coq_tactics tactics.
-From aneris Require Import lang lifting tactics proofmode notation network.
+From aneris.aneris_lang Require Import lang lifting tactics proofmode notation network.
 
 Set Default Proof Using "Type".
 
diff --git a/theories/aneris_lang/lib/vector_clock/vector_clock.v b/theories/aneris_lang/lib/vector_clock/vector_clock.v
index d73d84d6463c11187a29c78ddb92598be0494b3c..31f5c33447e9c585da254e17922417a89f91ea22 100644
--- a/theories/aneris_lang/lib/vector_clock/vector_clock.v
+++ b/theories/aneris_lang/lib/vector_clock/vector_clock.v
@@ -1,5 +1,5 @@
 From stdpp Require Export base list.
-From aneris Require Import lang lifting tactics proofmode notation adequacy.
+From aneris.aneris_lang Require Import lang lifting tactics proofmode notation adequacy.
 From aneris.aneris_lang.lib Require Export util network_helpers list.
 From aneris.aneris_lang.lib.serialization Require Export serialization.
 From aneris.aneris_lang.lib.vector_clock Require Export time.
diff --git a/theories/aneris_lang/system_state.v b/theories/aneris_lang/system_state.v
index 116045e55b0d2d5fd758cb7d7a102060c1d9f484..989aa939998037e602713614e4ec81d6a783eda8 100644
--- a/theories/aneris_lang/system_state.v
+++ b/theories/aneris_lang/system_state.v
@@ -3,7 +3,7 @@ From iris.base_logic Require Export gen_heap.
 From iris.base_logic.lib Require Export own.
 From iris.base_logic.lib Require Import fractional.
 From iris.proofmode Require Import tactics.
-From aneris Require Export lang network.
+From aneris.aneris_lang Require Export lang network.
 Set Default Proof Using "Type".
 Import uPred.
 Import Network.