diff --git a/saw-core-coq/coq/handwritten/CryptolToCoq/CryptolPrimitivesForSAWCoreExtra.v b/saw-core-coq/coq/handwritten/CryptolToCoq/CryptolPrimitivesForSAWCoreExtra.v
index f9c06ece50..46ed0cfa92 100644
--- a/saw-core-coq/coq/handwritten/CryptolToCoq/CryptolPrimitivesForSAWCoreExtra.v
+++ b/saw-core-coq/coq/handwritten/CryptolToCoq/CryptolPrimitivesForSAWCoreExtra.v
@@ -10,7 +10,7 @@ Import SAWCorePrelude.
 From CryptolToCoq Require Import SAWCorePreludeExtra.
 From CryptolToCoq Require Import SAWCoreVectorsAsCoqVectors.
 From CryptolToCoq Require Import CryptolPrimitivesForSAWCore.
-Import CryptolPrimitives.
+Import CryptolPrimitivesForSAWCore.
 
 Import ListNotations.