From 9cda6b33d667b861f371e89e7cccaf43135cfc7a Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 21 Apr 2022 12:29:24 +0200
Subject: Regenerate the test files

---
 tests/misc/External.Funs.fst | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'tests/misc/External.Funs.fst')

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
 
-- 
cgit v1.2.3