Merge branch 'son/clean' into checked-ops

1 files changed, 6 insertions, 6 deletions

diff --git a/tests/fstar/misc/PoloniusList.fst b/tests/fstar/misc/PoloniusList.fst
index b477802b..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_'a =
-        fun ret ->
-          let* tl1 = get_list_at_x_back ret in Return (List_Cons hd tl1) in
-      Return (l, back_'a)
-  | List_Nil -> Return (List_Nil, Return)
+      let back =
+        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