From ad55cb4128382852370ea53d36f4d21a83274e8b Mon Sep 17 00:00:00 2001
From: Kazuhiko Sakaguchi
Date: Thu, 10 Sep 2020 21:19:55 +0900
Subject: Turn class_of records into primitive records and get rid of the
 xclass idiom

---
 mathcomp/Make | 1 +
 1 file changed, 1 insertion(+)

(limited to 'mathcomp/Make')

diff --git a/mathcomp/Make b/mathcomp/Make
index 1d837c1..828a9e8 100644
--- a/mathcomp/Make
+++ b/mathcomp/Make
@@ -98,3 +98,4 @@ ssreflect/tuple.v
 -arg -w -arg -notation-overridden
 -arg -w -arg -duplicate-clear
 -arg -w -arg -ambiguous-paths
+-arg -w -arg +non-primitive-record
-- 
cgit v1.2.3