Skip to content

Commit 81fe35f

Browse files
committed
1 parent bb11e7f commit 81fe35f

File tree

2 files changed

+5
-1
lines changed

2 files changed

+5
-1
lines changed

theories/_CoqProject

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,2 +1,5 @@
11
-R . Stdlib
22
-arg -w -arg +default
3+
# to handle when requiring Rocq >= 9.2
4+
-arg -w -arg -notation-for-abbreviation
5+
-arg -w -arg -ltac2-notation-for-abbreviation

theories/dune

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -6,7 +6,8 @@
66
(env
77
(dev
88
(coq
9-
(flags :standard -w +default))))
9+
;; see theories/_CoqProject for details
10+
(flags :standard -w +default -w -notation-for-abbreviation -w -ltac2-notation-for-abbreviation))))
1011

1112
(rule
1213
(targets All.v)

0 commit comments

Comments
 (0)