diff options
author | Son Ho | 2023-12-23 00:59:55 +0100 |
---|---|---|
committer | Son Ho | 2023-12-23 00:59:55 +0100 |
commit | a4decc7654bc6f3301c0174124d21fdbc2dbc708 (patch) | |
tree | f992f3bb64609bf12d033a1424873a8134c66617 /tests/coq/misc/PoloniusList.v | |
parent | ff9fe8aa1e13a7297f7c4f2c2554235361db038f (diff) |
Regenerate the files
Diffstat (limited to 'tests/coq/misc/PoloniusList.v')
-rw-r--r-- | tests/coq/misc/PoloniusList.v | 8 |
1 files changed, 2 insertions, 6 deletions
diff --git a/tests/coq/misc/PoloniusList.v b/tests/coq/misc/PoloniusList.v index 7e967855..8f403a8e 100644 --- a/tests/coq/misc/PoloniusList.v +++ b/tests/coq/misc/PoloniusList.v @@ -27,9 +27,7 @@ Fixpoint get_list_at_x match ls with | List_Cons hd tl => if hd s= x - then - let back_'a := fun (ret : List_t u32) => Return ret in - Return (List_Cons hd tl, back_'a) + then Return (List_Cons hd tl, Return) else ( p <- get_list_at_x tl x; let (l, get_list_at_x_back) := p in @@ -37,9 +35,7 @@ Fixpoint get_list_at_x fun (ret : List_t u32) => tl1 <- get_list_at_x_back ret; Return (List_Cons hd tl1) in Return (l, back_'a)) - | List_Nil => - let back_'a := fun (ret : List_t u32) => Return ret in - Return (List_Nil, back_'a) + | List_Nil => Return (List_Nil, Return) end . |