fix build on Coq 8.17

kth-step · Jan 12, 2024 · 35d0187 · 35d0187
1 parent 0d4cf86
commit 35d0187
Show file tree

Hide file tree

Showing 2 changed files with 4 additions and 1 deletion.
diff --git a/_CoqProject b/_CoqProject
@@ -1,4 +1,6 @@
 -Q theories ABS
 
+-arg -w -arg -deprecated-hint-without-locality
+
 theories/abs_defs.v
 theories/abs_functional_metatheory.v
diff --git a/theories/dune b/theories/dune
@@ -1,7 +1,8 @@
 (coq.theory
  (name ABS)
  (package coq-abs-metatheory)
- (synopsis "Formal metatheory in Coq of the ABS language"))
+ (synopsis "Formal metatheory in Coq of the ABS language")
+ (flags :standard -w -deprecated-hint-without-locality))
 
 (rule
  (target abs_defs.v)