From 6eab7f1d8eeb7826d44c6bbacf24935965c8f7da Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Mon, 14 Nov 2022 09:33:19 +0100
Subject: Reactivate the option -test-trans-unis for Coq

---
 tests/coq/misc/External__Funs.v | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'tests')

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) :=
-- 
cgit v1.2.3