From 3a561145197762da371f4c32d2c47953e3d1afcd Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Fri, 6 May 2022 10:27:35 +0200
Subject: Regenerate the F* files for external.rs

---
 tests/misc/External.Funs.fst | 16 ++++++++++++++--
 1 file changed, 14 insertions(+), 2 deletions(-)

diff --git a/tests/misc/External.Funs.fst b/tests/misc/External.Funs.fst
index 3025da55..0ad40b00 100644
--- a/tests/misc/External.Funs.fst
+++ b/tests/misc/External.Funs.fst
@@ -11,7 +11,15 @@ include External.Opaque
 let swap_fwd (t : Type0) (x : t) (y : t) (st : state) : result (state & unit) =
   begin match core_mem_swap_fwd t x y st with
   | Fail -> Fail
-  | Return (st0, _) -> Return (st0, ())
+  | Return (st0, _) ->
+    begin match core_mem_swap_back0 t x y st with
+    | Fail -> Fail
+    | Return _ ->
+      begin match core_mem_swap_back1 t x y st with
+      | Fail -> Fail
+      | Return _ -> Return (st0, ())
+      end
+    end
   end
 
 (** [external::swap] *)
@@ -58,7 +66,11 @@ let custom_swap_fwd
   | Return (st0, _) ->
     begin match core_mem_swap_back0 t x y st with
     | Fail -> Fail
-    | Return x0 -> Return (st0, x0)
+    | Return x0 ->
+      begin match core_mem_swap_back1 t x y st with
+      | Fail -> Fail
+      | Return _ -> Return (st0, x0)
+      end
     end
   end
 
-- 
cgit v1.2.3