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/_CoqProject | 1 +
 1 file changed, 1 insertion(+)

(limited to 'mathcomp/_CoqProject')

diff --git a/mathcomp/_CoqProject b/mathcomp/_CoqProject
index 912cc1a..3b204ba 100644
--- a/mathcomp/_CoqProject
+++ b/mathcomp/_CoqProject
@@ -5,3 +5,4 @@
 -arg -w -arg -redundant-canonical-projection
 -arg -w -arg -notation-overridden
 -arg -w -arg -duplicate-clear
+-arg -w -arg +non-primitive-record
-- 
cgit v1.2.3