summaryrefslogtreecommitdiff
path: root/tests/misc/External.Opaque.fsti
diff options
context:
space:
mode:
authorSon Ho2022-05-04 15:39:29 +0200
committerSon Ho2022-05-04 15:39:29 +0200
commitcfd53959f31f0f9954ac84f130d069ed7a015a20 (patch)
treed4995f051051a2aaa307d8fcbad24d34e2219e87 /tests/misc/External.Opaque.fsti
parent15d90db02086f8ecae9a93ebf39c3c0ae8caa50f (diff)
Regenerate the F* files for the external.rs test
Diffstat (limited to 'tests/misc/External.Opaque.fsti')
-rw-r--r--tests/misc/External.Opaque.fsti4
1 files changed, 2 insertions, 2 deletions
diff --git a/tests/misc/External.Opaque.fsti b/tests/misc/External.Opaque.fsti
index 59c90b6b..b13a46eb 100644
--- a/tests/misc/External.Opaque.fsti
+++ b/tests/misc/External.Opaque.fsti
@@ -10,10 +10,10 @@ include External.Types
val core_mem_swap_fwd (t : Type0) : t -> t -> state -> result (state & unit)
(** [core::mem::swap] *)
-val core_mem_swap_back0 (t : Type0) : t -> t -> state -> result (state & t)
+val core_mem_swap_back0 (t : Type0) : t -> t -> state -> result t
(** [core::mem::swap] *)
-val core_mem_swap_back1 (t : Type0) : t -> t -> state -> result (state & t)
+val core_mem_swap_back1 (t : Type0) : t -> t -> state -> result t
(** [core::num::nonzero::NonZeroU32::{14}::new] *)
val core_num_nonzero_non_zero_u32_14_new_fwd