Implement two phases of loops join + collapse

1 files changed, 1 insertions, 26 deletions

diff --git a/tests/coq/demo/Demo.v b/tests/coq/demo/Demo.v
index 8d8f840d..14b1ca9d 100644
--- a/tests/coq/demo/Demo.v
+++ b/tests/coq/demo/Demo.v
@@ -90,38 +90,13 @@ Fixpoint list_nth_mut
   end
 .
 
-(** [demo::list_nth_mut1]: loop 0:
-    Source: 'tests/src/demo.rs', lines 69:0-78:1 *)
-Fixpoint list_nth_mut1_loop
-  (T : Type) (n : nat) (l : CList_t T) (i : u32) :
-  result (T * (T -> result (CList_t T)))
-  :=
-  match n with
-  | O => Fail_ OutOfFuel
-  | S n1 =>
-    match l with
-    | CList_CCons x tl =>
-      if i s= 0%u32
-      then let back := fun (ret : T) => Ok (CList_CCons ret tl) in Ok (x, back)
-      else (
-        i1 <- u32_sub i 1%u32;
-        p <- list_nth_mut1_loop T n1 tl i1;
-        let (t, back) := p in
-        let back1 := fun (ret : T) => tl1 <- back ret; Ok (CList_CCons x tl1)
-          in
-        Ok (t, back1))
-    | CList_CNil => Fail_ Failure
-    end
-  end
-.
-
 (** [demo::list_nth_mut1]:
     Source: 'tests/src/demo.rs', lines 69:0-69:77 *)
 Definition list_nth_mut1
   (T : Type) (n : nat) (l : CList_t T) (i : u32) :
   result (T * (T -> result (CList_t T)))
   :=
-  list_nth_mut1_loop T n l i
+  admit
 .
 
 (** [demo::i32_id]: