Fix an issue with the translation of loops::clear

2 files changed, 6 insertions, 16 deletions

diff --git a/tests/coq/misc/Loops.v b/tests/coq/misc/Loops.v
index ec8fa39c..29f312bf 100644
--- a/tests/coq/misc/Loops.v
+++ b/tests/coq/misc/Loops.v
@@ -63,7 +63,7 @@ Definition sum_with_shared_borrows_fwd (n : nat) (max : u32) : result u32 :=
 .
 
 (** [loops::clear] *)
-Definition clear_loop_fwd_back
+Fixpoint clear_loop_fwd_back
   (n : nat) (v : vec u32) (i : usize) : result (vec u32) :=
   match n with
   | O => Fail_ OutOfFuel
@@ -73,16 +73,14 @@ Definition clear_loop_fwd_back
     then (
       i1 <- usize_add i 1%usize;
       v0 <- vec_index_mut_back u32 v i (0%u32);
-      v1 <- clear_loop_fwd n0 v0 i1;
-      let _ := v1 in
-      Return v0)
+      clear_loop_fwd_back n0 v0 i1)
     else Return v
   end
 .
 
 (** [loops::clear] *)
 Definition clear_fwd_back (n : nat) (v : vec u32) : result (vec u32) :=
-  v0 <- clear_loop_fwd n v (0%usize); let _ := v0 in Return v
+  clear_loop_fwd_back n v (0%usize)
 .
 
 (** [loops::List] *)
diff --git a/tests/fstar/misc/Loops.Funs.fst b/tests/fstar/misc/Loops.Funs.fst
index d19e9328..c0aca975 100644
--- a/tests/fstar/misc/Loops.Funs.fst
+++ b/tests/fstar/misc/Loops.Funs.fst
@@ -70,7 +70,7 @@ let sum_with_shared_borrows_fwd (max : u32) : result u32 =
   sum_with_shared_borrows_loop_fwd max 0 0
 
 (** [loops::clear] *)
-let clear_loop_fwd_back
+let rec clear_loop_fwd_back
   (v : vec u32) (i : usize) :
   Tot (result (vec u32)) (decreases (clear_decreases v i))
   =
@@ -82,21 +82,13 @@ let clear_loop_fwd_back
     | Return i1 ->
       begin match vec_index_mut_back u32 v i 0 with
       | Fail e -> Fail e
-      | Return v0 ->
-        begin match clear_loop_fwd v0 i1 with
-        | Fail e -> Fail e
-        | Return _ -> Return v0
-        end
+      | Return v0 -> clear_loop_fwd_back v0 i1
       end
     end
   else Return v
 
 (** [loops::clear] *)
-let clear_fwd_back (v : vec u32) : result (vec u32) =
-  begin match clear_loop_fwd v 0 with
-  | Fail e -> Fail e
-  | Return _ -> Return v
-  end
+let clear_fwd_back (v : vec u32) : result (vec u32) = clear_loop_fwd_back v 0
 
 (** [loops::list_mem] *)
 let rec list_mem_loop_fwd