diff options
Diffstat (limited to 'tests')
| -rw-r--r-- | tests/coq/misc/External__Funs.v | 3 |
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) := |