summaryrefslogtreecommitdiff
path: root/tests/coq/traits/Traits.v
diff options
context:
space:
mode:
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]: