From 11817ca4ec2d681047ad59d1037b13674670b0e3 Mon Sep 17 00:00:00 2001 From: Tahina Ramananandro Date: Mon, 25 Nov 2024 08:48:18 -0800 Subject: [PATCH] mark type abbreviations inline_for_extraction --- src/cbor/pulse/CBOR.Pulse.API.Det.Type.fsti | 4 ++++ src/cbor/pulse/CBOR.Pulse.Type.fst | 2 ++ 2 files changed, 6 insertions(+) diff --git a/src/cbor/pulse/CBOR.Pulse.API.Det.Type.fsti b/src/cbor/pulse/CBOR.Pulse.API.Det.Type.fsti index 150008ad..916610d7 100644 --- 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 index 03734bc4..d110257c 100644 --- 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