@@ -226,7 +226,7 @@ namespace FFI_Export
226 %used FFI_Prim prim
226 %used FFI_Prim prim
228 data FFI_Exportable : (f : FFI) -> List (Type, ffi_data f) -> Type -> Type where
228 data FFI_Exportable : (f : FFI) -> List (Type, ffi_data f) -> Type -> Type where
229− FFI_IO : (b : FFI_Base f xs t) -> FFI_Exportable f xs (IO t)
229+ FFI_IO : (b : FFI_Base f xs t) -> FFI_Exportable f xs (IO' f t)
230 FFI_Fun : (b : FFI_Base f xs s) -> (a : FFI_Exportable f xs t) -> FFI_Exportable f xs (s -> t)
230 FFI_Fun : (b : FFI_Base f xs s) -> (a : FFI_Exportable f xs t) -> FFI_Exportable f xs (s -> t)
231 FFI_Ret : (b : FFI_Base f xs t) -> FFI_Exportable f xs t
231 FFI_Ret : (b : FFI_Base f xs t) -> FFI_Exportable f xs t