aboutsummaryrefslogtreecommitdiff
path: root/_CoqProject
diff options
context:
space:
mode:
Diffstat (limited to '_CoqProject')
-rw-r--r--_CoqProject10
1 files changed, 10 insertions, 0 deletions
diff --git a/_CoqProject b/_CoqProject
new file mode 100644
index 0000000..5493330
--- /dev/null
+++ b/_CoqProject
@@ -0,0 +1,10 @@
+-I mathcomp
+-R mathcomp mathcomp
+
+-arg -w -arg -projection-no-head-constant
+-arg -w -arg -redundant-canonical-projection
+-arg -w -arg -notation-overridden
+-arg -w -arg +duplicate-clear
+-arg -w -arg +non-primitive-record
+-arg -w -arg +undeclared-scope
+-arg -w -arg -deprecated-hint-without-locality