diff options
| -rw-r--r-- | Makefile | 4 | ||||
| -rw-r--r-- | tests/coq/misc/External__Funs.v | 3 |
2 files changed, 4 insertions, 3 deletions
@@ -198,10 +198,8 @@ tfstarp-%: BACKEND_SUBDIR := fstar tfstarp-%: $(AENEAS_CMD) -# TODO: -test-trans-units -# It doesn't work on vec_push_fwd, I don't understand why. .PHONY: tcoq-% -tcoq-%: OPTIONS += -backend coq +tcoq-%: OPTIONS += -backend coq -test-trans-units tcoq-%: BACKEND_SUBDIR := coq tcoq-%: $(AENEAS_CMD) 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) := |