7 files changed, 9 insertions, 9 deletions
diff --git a/Everything.agda b/Everything.agda
index d547bcd..f6c6f84 100644
--- a/Everything.agda
+++ b/Everything.agda
@@ -48,6 +48,9 @@ import Helium.Algebra.Ordered.StrictTotal.Structures
 -- Some more algebraic structures
 import Helium.Algebra.Structures
 
+-- Definition of types and operations used by the Armv8-M pseudocode.
+import Helium.Data.Pseudocode.Algebra
+
 -- Definition of the Armv8-M pseudocode.
 import Helium.Data.Pseudocode.Core
 
@@ -57,9 +60,6 @@ import Helium.Data.Pseudocode.Manipulate
 -- Basic properties of the pseudocode data types
 import Helium.Data.Pseudocode.Properties
 
--- Definition of types and operations used by the Armv8-M pseudocode.
-import Helium.Data.Pseudocode.Types
-
 -- Definition of instructions using the Armv8-M pseudocode.
 import Helium.Instructions.Base
 
diff --git a/src/Helium/Data/Pseudocode/Types.agda b/src/Helium/Data/Pseudocode/Algebra.agda
index 6ea9cd2..523150d 100644
--- a/src/Helium/Data/Pseudocode/Types.agda
+++ b/src/Helium/Data/Pseudocode/Algebra.agda
@@ -6,7 +6,7 @@
 
 {-# OPTIONS --safe --without-K #-}
 
-module Helium.Data.Pseudocode.Types where
+module Helium.Data.Pseudocode.Algebra where
 
 open import Algebra.Core
 import Algebra.Definitions.RawSemiring as RS
diff --git a/src/Helium/Semantics/Axiomatic/Assertion.agda b/src/Helium/Semantics/Axiomatic/Assertion.agda
index 8192e5f..ab786e5 100644
--- a/src/Helium/Semantics/Axiomatic/Assertion.agda
+++ b/src/Helium/Semantics/Axiomatic/Assertion.agda
@@ -6,7 +6,7 @@
 
 {-# OPTIONS --safe --without-K #-}
 
-open import Helium.Data.Pseudocode.Types using (RawPseudocode)
+open import Helium.Data.Pseudocode.Algebra using (RawPseudocode)
 
 module Helium.Semantics.Axiomatic.Assertion
   {b₁ b₂ i₁ i₂ i₃ r₁ r₂ r₃}
diff --git a/src/Helium/Semantics/Axiomatic/Core.agda b/src/Helium/Semantics/Axiomatic/Core.agda
index 3b7e8db..a65a6d0 100644
--- a/src/Helium/Semantics/Axiomatic/Core.agda
+++ b/src/Helium/Semantics/Axiomatic/Core.agda
@@ -6,7 +6,7 @@
 
 {-# OPTIONS --safe --without-K #-}
 
-open import Helium.Data.Pseudocode.Types using (RawPseudocode)
+open import Helium.Data.Pseudocode.Algebra using (RawPseudocode)
 
 module Helium.Semantics.Axiomatic.Core
   {b₁ b₂ i₁ i₂ i₃ r₁ r₂ r₃}
diff --git a/src/Helium/Semantics/Axiomatic/Term.agda b/src/Helium/Semantics/Axiomatic/Term.agda
index 2719455..57dad92 100644
--- a/src/Helium/Semantics/Axiomatic/Term.agda
+++ b/src/Helium/Semantics/Axiomatic/Term.agda
@@ -6,7 +6,7 @@
 
 {-# OPTIONS --safe --without-K #-}
 
-open import Helium.Data.Pseudocode.Types using (RawPseudocode)
+open import Helium.Data.Pseudocode.Algebra using (RawPseudocode)
 
 module Helium.Semantics.Axiomatic.Term
   {b₁ b₂ i₁ i₂ i₃ r₁ r₂ r₃}
diff --git a/src/Helium/Semantics/Axiomatic/Triple.agda b/src/Helium/Semantics/Axiomatic/Triple.agda
index 7564983..23a487e 100644
--- a/src/Helium/Semantics/Axiomatic/Triple.agda
+++ b/src/Helium/Semantics/Axiomatic/Triple.agda
@@ -6,7 +6,7 @@
 
 {-# OPTIONS --safe --without-K #-}
 
-open import Helium.Data.Pseudocode.Types using (RawPseudocode)
+open import Helium.Data.Pseudocode.Algebra using (RawPseudocode)
 
 module Helium.Semantics.Axiomatic.Triple
   {b₁ b₂ i₁ i₂ i₃ r₁ r₂ r₃}
diff --git a/src/Helium/Semantics/Denotational/Core.agda b/src/Helium/Semantics/Denotational/Core.agda
index 0bd1794..090e0ba 100644
--- a/src/Helium/Semantics/Denotational/Core.agda
+++ b/src/Helium/Semantics/Denotational/Core.agda
@@ -6,7 +6,7 @@
 
 {-# OPTIONS --safe --without-K #-}
 
-open import Helium.Data.Pseudocode.Types using (RawPseudocode)
+open import Helium.Data.Pseudocode.Algebra using (RawPseudocode)
 
 module Helium.Semantics.Denotational.Core
   {b₁ b₂ i₁ i₂ i₃ r₁ r₂ r₃}