mark type abbreviations inline_for_extraction

project-everest · Nov 25, 2024 · 11817ca · 11817ca
1 parent a517db7
commit 11817ca
Show file tree

Hide file tree

Showing 2 changed files with 6 additions and 0 deletions.
diff --git a/src/cbor/pulse/CBOR.Pulse.API.Det.Type.fsti b/src/cbor/pulse/CBOR.Pulse.API.Det.Type.fsti
@@ -1,10 +1,14 @@
 module CBOR.Pulse.API.Det.Type
 
 inline_for_extraction
+noextract [@@noextract_to "krml"]
 val cbor_det_t: Type0
 inline_for_extraction
+noextract [@@noextract_to "krml"]
 val cbor_det_map_entry_t: Type0
 inline_for_extraction
+noextract [@@noextract_to "krml"]
 val cbor_det_array_iterator_t: Type0
 inline_for_extraction
+noextract [@@noextract_to "krml"]
 val cbor_det_map_iterator_t: Type0
diff --git a/src/cbor/pulse/CBOR.Pulse.Type.fst b/src/cbor/pulse/CBOR.Pulse.Type.fst
@@ -103,9 +103,11 @@ type cbor_raw_iterator (elt: Type0) =
 | CBOR_Raw_Iterator_Serialized of cbor_raw_serialized_iterator
 
 inline_for_extraction
+noextract [@@noextract_to "krml"]
 let cbor_array_iterator
 = cbor_raw_iterator cbor_raw
 
 inline_for_extraction
+noextract [@@noextract_to "krml"]
 let cbor_map_iterator
 = cbor_raw_iterator cbor_map_entry