Disable “hiding-demiting-key” warnings

jasmin-lang · Nov 21, 2023 · cbb2ecf · cbb2ecf
1 parent 62481d8
commit cbb2ecf
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 0 deletions.
diff --git a/_CoqProject b/_CoqProject
@@ -2,5 +2,6 @@
 -arg -w -arg -notation-overridden
 -arg -w -arg -redundant-canonical-projection
 -arg -w -arg -projection-no-head-constant
+-arg "-w -hiding-delimiting-key"
 
 -R _build/default/src mathcomp.word
diff --git a/src/dune b/src/dune
@@ -2,6 +2,7 @@
  (name mathcomp.word)
  (package coq-mathcomp-word)
  (flags -w -ambiguous-paths
+        -w -hiding-delimiting-key
         -w -notation-overridden
         -w -redundant-canonical-projection
         -w -projection-no-head-constant))