Merge pull request #464 from FStarLang/_taramana_dpe_cbor

DPE example: CBOR.Spec.Constants -> CBOR.Spec.Const

Author: tahina-pro

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

share/pulse/examples/dice/cbor/CBOR.Spec.Constants.fst renamed to 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
 

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

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