diff options
| author | Son Ho | 2022-11-14 11:58:31 +0100 |
|---|---|---|
| committer | Son HO | 2022-11-14 14:21:04 +0100 |
| commit | 5a96e28b8706ed945ccbb569881ca1888cd73ace (patch) | |
| tree | 9e48a9c0b50f96a413f874c90919c90ffbefc0cb /tests/coq/misc/External__Funs.v | |
| parent | 868fa924a37a3af6e701bbc0a2d51fefc2dc7c33 (diff) | |
Regenerate the files and fix the proofs
Diffstat (limited to 'tests/coq/misc/External__Funs.v')
| -rw-r--r-- | tests/coq/misc/External__Funs.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tests/coq/misc/External__Funs.v b/tests/coq/misc/External__Funs.v index cd03ae3d..cc9e9461 100644 --- a/tests/coq/misc/External__Funs.v +++ b/tests/coq/misc/External__Funs.v @@ -107,7 +107,7 @@ Definition test_swap_non_zero_fwd p0 <- swap_back u32 x (0 %u32) st st0; let (st1, p1) := p0 in let (x0, _) := p1 in - if x0 s= 0 %u32 then Fail_ else Return (st1, x0) + if x0 s= 0 %u32 then Fail_ Failure else Return (st1, x0) . End External__Funs . |