diff options
Diffstat (limited to 'tests/coq/misc/Loops.v')
| -rw-r--r-- | tests/coq/misc/Loops.v | 78 |
1 files changed, 39 insertions, 39 deletions
diff --git a/tests/coq/misc/Loops.v b/tests/coq/misc/Loops.v index 7c83a014..ae529cf8 100644 --- a/tests/coq/misc/Loops.v +++ b/tests/coq/misc/Loops.v @@ -375,18 +375,18 @@ Fixpoint list_nth_mut_loop_pair_loop | List_Cons x1 tl1 => if i s= 0%u32 then - let back_'a := fun (ret : T) => Return (List_Cons ret tl0) in - let back_'b := fun (ret : T) => Return (List_Cons ret tl1) in - Return ((x0, x1), back_'a, back_'b) + let back'a := fun (ret : T) => Return (List_Cons ret tl0) in + let back'b := fun (ret : T) => Return (List_Cons ret tl1) in + Return ((x0, x1), back'a, back'b) else ( i1 <- u32_sub i 1%u32; t <- list_nth_mut_loop_pair_loop T n1 tl0 tl1 i1; - let '(p, back_'a, back_'b) := t in - let back_'a1 := - fun (ret : T) => tl01 <- back_'a ret; Return (List_Cons x0 tl01) in - let back_'b1 := - fun (ret : T) => tl11 <- back_'b ret; Return (List_Cons x1 tl11) in - Return (p, back_'a1, back_'b1)) + let '(p, back'a, back'b) := t in + let back'a1 := + fun (ret : T) => tl01 <- back'a ret; Return (List_Cons x0 tl01) in + let back'b1 := + fun (ret : T) => tl11 <- back'b ret; Return (List_Cons x1 tl11) in + Return (p, back'a1, back'b1)) | List_Nil => Fail_ Failure end | List_Nil => Fail_ Failure @@ -451,21 +451,21 @@ Fixpoint list_nth_mut_loop_pair_merge_loop | List_Cons x1 tl1 => if i s= 0%u32 then - let back_'a := + let back := fun (ret : (T * T)) => let (t, t1) := ret in Return (List_Cons t tl0, List_Cons t1 tl1) in - Return ((x0, x1), back_'a) + Return ((x0, x1), back) else ( i1 <- u32_sub i 1%u32; p <- list_nth_mut_loop_pair_merge_loop T n1 tl0 tl1 i1; - let (p1, back_'a) := p in - let back_'a1 := + let (p1, back) := p in + let back1 := fun (ret : (T * T)) => - p2 <- back_'a ret; + p2 <- back ret; let (tl01, tl11) := p2 in Return (List_Cons x0 tl01, List_Cons x1 tl11) in - Return (p1, back_'a1)) + Return (p1, back1)) | List_Nil => Fail_ Failure end | List_Nil => Fail_ Failure @@ -531,15 +531,15 @@ Fixpoint list_nth_mut_shared_loop_pair_loop | List_Cons x1 tl1 => if i s= 0%u32 then - let back_'a := fun (ret : T) => Return (List_Cons ret tl0) in - Return ((x0, x1), back_'a) + let back := fun (ret : T) => Return (List_Cons ret tl0) in + Return ((x0, x1), back) else ( i1 <- u32_sub i 1%u32; p <- list_nth_mut_shared_loop_pair_loop T n1 tl0 tl1 i1; - let (p1, back_'a) := p in - let back_'a1 := - fun (ret : T) => tl01 <- back_'a ret; Return (List_Cons x0 tl01) in - Return (p1, back_'a1)) + let (p1, back) := p in + let back1 := + fun (ret : T) => tl01 <- back ret; Return (List_Cons x0 tl01) in + Return (p1, back1)) | List_Nil => Fail_ Failure end | List_Nil => Fail_ Failure @@ -571,15 +571,15 @@ Fixpoint list_nth_mut_shared_loop_pair_merge_loop | List_Cons x1 tl1 => if i s= 0%u32 then - let back_'a := fun (ret : T) => Return (List_Cons ret tl0) in - Return ((x0, x1), back_'a) + let back := fun (ret : T) => Return (List_Cons ret tl0) in + Return ((x0, x1), back) else ( i1 <- u32_sub i 1%u32; p <- list_nth_mut_shared_loop_pair_merge_loop T n1 tl0 tl1 i1; - let (p1, back_'a) := p in - let back_'a1 := - fun (ret : T) => tl01 <- back_'a ret; Return (List_Cons x0 tl01) in - Return (p1, back_'a1)) + let (p1, back) := p in + let back1 := + fun (ret : T) => tl01 <- back ret; Return (List_Cons x0 tl01) in + Return (p1, back1)) | List_Nil => Fail_ Failure end | List_Nil => Fail_ Failure @@ -611,15 +611,15 @@ Fixpoint list_nth_shared_mut_loop_pair_loop | List_Cons x1 tl1 => if i s= 0%u32 then - let back_'b := fun (ret : T) => Return (List_Cons ret tl1) in - Return ((x0, x1), back_'b) + let back := fun (ret : T) => Return (List_Cons ret tl1) in + Return ((x0, x1), back) else ( i1 <- u32_sub i 1%u32; p <- list_nth_shared_mut_loop_pair_loop T n1 tl0 tl1 i1; - let (p1, back_'b) := p in - let back_'b1 := - fun (ret : T) => tl11 <- back_'b ret; Return (List_Cons x1 tl11) in - Return (p1, back_'b1)) + let (p1, back) := p in + let back1 := + fun (ret : T) => tl11 <- back ret; Return (List_Cons x1 tl11) in + Return (p1, back1)) | List_Nil => Fail_ Failure end | List_Nil => Fail_ Failure @@ -651,15 +651,15 @@ Fixpoint list_nth_shared_mut_loop_pair_merge_loop | List_Cons x1 tl1 => if i s= 0%u32 then - let back_'a := fun (ret : T) => Return (List_Cons ret tl1) in - Return ((x0, x1), back_'a) + let back := fun (ret : T) => Return (List_Cons ret tl1) in + Return ((x0, x1), back) else ( i1 <- u32_sub i 1%u32; p <- list_nth_shared_mut_loop_pair_merge_loop T n1 tl0 tl1 i1; - let (p1, back_'a) := p in - let back_'a1 := - fun (ret : T) => tl11 <- back_'a ret; Return (List_Cons x1 tl11) in - Return (p1, back_'a1)) + let (p1, back) := p in + let back1 := + fun (ret : T) => tl11 <- back ret; Return (List_Cons x1 tl11) in + Return (p1, back1)) | List_Nil => Fail_ Failure end | List_Nil => Fail_ Failure |