From b455f94c841b2423898f39bc9b6a4c35a3db56e3 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 4 Apr 2024 16:20:20 +0200
Subject: Regenerate the test files

---
 tests/fstar/misc/PoloniusList.fst | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

(limited to 'tests/fstar/misc/PoloniusList.fst')

diff --git a/tests/fstar/misc/PoloniusList.fst b/tests/fstar/misc/PoloniusList.fst
index 4203247e..c0bc592e 100644
--- a/tests/fstar/misc/PoloniusList.fst
+++ b/tests/fstar/misc/PoloniusList.fst
@@ -20,13 +20,13 @@ let rec get_list_at_x
   begin match ls with
   | List_Cons hd tl ->
     if hd = x
-    then Return (List_Cons hd tl, Return)
+    then Ok (List_Cons hd tl, Ok)
     else
       let* (l, get_list_at_x_back) = get_list_at_x tl x in
       let back =
-        fun ret ->
-          let* tl1 = get_list_at_x_back ret in Return (List_Cons hd tl1) in
-      Return (l, back)
-  | List_Nil -> Return (List_Nil, Return)
+        fun ret -> let* tl1 = get_list_at_x_back ret in Ok (List_Cons hd tl1)
+        in
+      Ok (l, back)
+  | List_Nil -> Ok (List_Nil, Ok)
   end
 
-- 
cgit v1.2.3