diff --git a/share/pulse/examples/dice/cbor/CBOR.Pulse.fst b/share/pulse/examples/dice/cbor/CBOR.Pulse.fst
index 9b1f20d35..5d6446fcc 100644
--- a/share/pulse/examples/dice/cbor/CBOR.Pulse.fst
+++ b/share/pulse/examples/dice/cbor/CBOR.Pulse.fst
@@ -16,7 +16,7 @@
 
 module CBOR.Pulse
 #lang-pulse
-include CBOR.Spec.Constants
+include CBOR.Spec.Const
 include CBOR.Pulse.Extern
 open Pulse.Lib.Pervasives
 open Pulse.Lib.Trade
diff --git a/share/pulse/examples/dice/cbor/CBOR.Spec.Constants.fst b/share/pulse/examples/dice/cbor/CBOR.Spec.Const.fst
similarity index 98%
rename from share/pulse/examples/dice/cbor/CBOR.Spec.Constants.fst
rename to share/pulse/examples/dice/cbor/CBOR.Spec.Const.fst
index 1c55a4cec..113e6f922 100644
--- a/share/pulse/examples/dice/cbor/CBOR.Spec.Constants.fst
+++ b/share/pulse/examples/dice/cbor/CBOR.Spec.Const.fst
@@ -14,7 +14,7 @@
    limitations under the License.
 *)
 
-module CBOR.Spec.Constants
+module CBOR.Spec.Const
 
 module U8 = FStar.UInt8
 
diff --git a/share/pulse/examples/dice/cbor/CBOR.Spec.Type.fsti b/share/pulse/examples/dice/cbor/CBOR.Spec.Type.fsti
index 5d33f6bc8..fe13a74b0 100644
--- a/share/pulse/examples/dice/cbor/CBOR.Spec.Type.fsti
+++ b/share/pulse/examples/dice/cbor/CBOR.Spec.Type.fsti
@@ -15,7 +15,7 @@
 *)
 
 module CBOR.Spec.Type
-include CBOR.Spec.Constants
+include CBOR.Spec.Const
 
 module U8 = FStar.UInt8
 module U64 = FStar.UInt64
diff --git a/share/pulse/examples/dice/cbor/Makefile b/share/pulse/examples/dice/cbor/Makefile
index c8fc623ba..605b459b0 100644
--- a/share/pulse/examples/dice/cbor/Makefile
+++ b/share/pulse/examples/dice/cbor/Makefile
@@ -34,7 +34,7 @@ extract_all_ml: $(ALL_ML_FILES)
 extract_c: $(OUTPUT_DIR)/CBOR.h
 
 $(OUTPUT_DIR)/CBOR.h: $(ALL_KRML_FILES)
-	$(KRML) -bundle C -bundle CBOR.Spec.Constants+CBOR.Pulse.Type+CBOR.Pulse.Extern=[rename=CBOR] -no-prefix CBOR.Spec.Constants,CBOR.Pulse.Type,CBOR.Pulse.Extern -bundle CBOR.Pulse= -bundle CDDLExtractionTest.Assume+CDDLExtractionTest.Bytes+CDDLExtractionTest.BytesUnwrapped+CDDLExtractionTest.Choice=*[rename=CDDLExtractionTest] -skip-linking $^ -tmpdir $(OUTPUT_DIR)
+	$(KRML) -bundle C -bundle CBOR.Spec.Const+CBOR.Pulse.Type+CBOR.Pulse.Extern=[rename=CBOR] -no-prefix CBOR.Spec.Const,CBOR.Pulse.Type,CBOR.Pulse.Extern -bundle CBOR.Pulse= -bundle CDDLExtractionTest.Assume+CDDLExtractionTest.Bytes+CDDLExtractionTest.BytesUnwrapped+CDDLExtractionTest.Choice=*[rename=CDDLExtractionTest] -skip-linking $^ -tmpdir $(OUTPUT_DIR)
 
 .PHONY: extern