summaryrefslogtreecommitdiff
path: root/tests/coq/traits
diff options
context:
space:
mode:
authorSon Ho2023-12-23 00:59:55 +0100
committerSon Ho2023-12-23 00:59:55 +0100
commita4decc7654bc6f3301c0174124d21fdbc2dbc708 (patch)
treef992f3bb64609bf12d033a1424873a8134c66617 /tests/coq/traits
parentff9fe8aa1e13a7297f7c4f2c2554235361db038f (diff)
Regenerate the files
Diffstat (limited to '')
-rw-r--r--tests/coq/traits/Traits.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/tests/coq/traits/Traits.v b/tests/coq/traits/Traits.v
index 7055e25d..7abf2021 100644
--- a/tests/coq/traits/Traits.v
+++ b/tests/coq/traits/Traits.v
@@ -334,7 +334,7 @@ Definition use_with_const_ty1
(H : Type) (LEN : usize) (withConstTyHLENInst : WithConstTy_t H LEN) :
result usize
:=
- let i := withConstTyHLENInst.(WithConstTy_tWithConstTy_t_LEN1) in Return i
+ Return withConstTyHLENInst.(WithConstTy_tWithConstTy_t_LEN1)
.
(** [traits::use_with_const_ty2]: