summaryrefslogtreecommitdiff
path: root/tests/misc/External.Funs.fst
diff options
context:
space:
mode:
Diffstat (limited to 'tests/misc/External.Funs.fst')
-rw-r--r--tests/misc/External.Funs.fst2
1 files changed, 1 insertions, 1 deletions
diff --git a/tests/misc/External.Funs.fst b/tests/misc/External.Funs.fst
index 927dad9c..57e9deee 100644
--- a/tests/misc/External.Funs.fst
+++ b/tests/misc/External.Funs.fst
@@ -22,7 +22,7 @@ let swap_back
| Return (st0, x0) ->
begin match core_mem_swap_back1 t x y st0 with
| Fail -> Fail
- | Return (st1, x1) -> Return (st1, (x0, x1))
+ | Return (st1, y0) -> Return (st1, (x0, y0))
end
end