From 9c693eedb8e7e11aeaedbd3ce79a9478b10be7c8 Mon Sep 17 00:00:00 2001
From: Cyril Cohen
Date: Tue, 24 Nov 2020 23:14:22 +0100
Subject: Using `only printing` and fixing coercion in notations

---
 mathcomp/Makefile.test-suite.coq.local | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'mathcomp/Makefile.test-suite.coq.local')

diff --git a/mathcomp/Makefile.test-suite.coq.local b/mathcomp/Makefile.test-suite.coq.local
index 2de68fc..c9604ab 100644
--- a/mathcomp/Makefile.test-suite.coq.local
+++ b/mathcomp/Makefile.test-suite.coq.local
@@ -1,4 +1,4 @@
-OUTPUT_TESTS=test_suite/output.v
+OUTPUT_TESTS=test_suite/output.v test_suite/imset2_finset.v test_suite/imset2_gproduct.v
 
 OUTPUT_ARTIFACTS=$(OUTPUT_TESTS:%.v=%.v.out.new)
 
-- 
cgit v1.2.3