summaryrefslogtreecommitdiff
path: root/tests/coq
diff options
context:
space:
mode:
Diffstat (limited to 'tests/coq')
-rw-r--r--tests/coq/misc/External__Funs.v3
1 files changed, 1 insertions, 2 deletions
diff --git a/tests/coq/misc/External__Funs.v b/tests/coq/misc/External__Funs.v
index 77b738b0..df35f7eb 100644
--- a/tests/coq/misc/External__Funs.v
+++ b/tests/coq/misc/External__Funs.v
@@ -84,8 +84,7 @@ Definition test_custom_swap_back
result (state * (u32 * u32))
:=
p <- custom_swap_back u32 x y st (1 %u32) st0;
- let (st1, tmp) := p in
- let (x0, y0) := tmp in Return (st1, (x0, y0))
+ let (st1, (x0, y0)) := p in Return (st1, (x0, y0))
.
(** [external::test_swap_non_zero] *)