aboutsummaryrefslogtreecommitdiff
path: root/_CoqProject
diff options
context:
space:
mode:
authorCyril Cohen2021-03-14 22:31:40 +0100
committerCyril Cohen2021-03-15 02:08:56 +0100
commit25695dba0365a252cb142d5ba9079bd59f3ccad2 (patch)
tree8e7807356032b9e88aafb4725e5cc5d408038ebc /_CoqProject
parentdeb0e19892674652b430b3cb89259bb5afc089b8 (diff)
fixup gitpod config
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