summaryrefslogtreecommitdiff
path: root/tests
diff options
context:
space:
mode:
Diffstat (limited to 'tests')
-rw-r--r--tests/coq/misc/External__Funs.v3
1 files changed, 3 insertions, 0 deletions
diff --git a/tests/coq/misc/External__Funs.v b/tests/coq/misc/External__Funs.v
index e8ecfab8..cd03ae3d 100644
--- a/tests/coq/misc/External__Funs.v
+++ b/tests/coq/misc/External__Funs.v
@@ -54,6 +54,9 @@ Definition test_vec_fwd : result unit :=
Return tt
.
+(** Unit test for [external::test_vec] *)
+Check (test_vec_fwd )%return.
+
(** [external::custom_swap] *)
Definition custom_swap_fwd
(T : Type) (x : T) (y : T) (st : state) : result (state * T) :=