diff --git a/formal/SilverSight/Receipt.lean b/formal/SilverSight/Receipt.lean
index f5a07e8d..a7700ea2 100644
--- a/formal/SilverSight/Receipt.lean
+++ b/formal/SilverSight/Receipt.lean
@@ -1,9 +1,9 @@
-import Semantics.FixedPoint
+import SilverSight.FixedPoint
 
 namespace SilverSight
 
-open Semantics.FixedPoint
-open Semantics.FixedPoint.Q16_16
+open SilverSight.FixedPoint
+open SilverSight.FixedPoint.Q16_16
 
 -- ═══════════════════════════════════════════════════════════════════════════
 -- §1  Gate types
diff --git a/formal/SilverSight/Schema.lean b/formal/SilverSight/Schema.lean
index c9594db3..06bd3462 100644
--- a/formal/SilverSight/Schema.lean
+++ b/formal/SilverSight/Schema.lean
@@ -1,8 +1,8 @@
-import Semantics.FixedPoint
+import SilverSight.FixedPoint
 
 namespace SilverSight
 
-open Semantics.FixedPoint
+open SilverSight.FixedPoint
 
 /-- A Schema describes the wire-level layout of a type:
     - `byteSize`: the number of bytes in the wire representation