-
Notifications
You must be signed in to change notification settings - Fork 2
Expand file tree
/
Copy path_CoqProject
More file actions
26 lines (23 loc) · 1.03 KB
/
_CoqProject
File metadata and controls
26 lines (23 loc) · 1.03 KB
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
# AUTO-GENERATED CONTENT, EDIT `gen-_CoqProject-dune.sh` INSTEAD
# Avoid warnings about entries in this _CoqProject
-arg -w -arg -cannot-open-path
# Warning settings from `dune` project files
-arg -w -arg -notation-overridden
-arg -w -arg -custom-entry-overridden
-arg -w -arg -redundant-canonical-projection
-arg -w -arg -ambiguous-paths
-arg -w -arg -notation-incompatible-prefix
# Turn warning on hints into error:
-arg -w -arg +deprecated-hint-without-locality
-arg -w -arg +deprecated-instance-without-locality
-arg -w -arg +deprecated-tacopt-without-locality
-arg -w -arg +future-coercion-class-field
-arg -w -arg +unknown-option
-arg -w -arg +sl-transparent-constants
# Plugin directory.
-I _build/install/default/lib
# Specified logical paths for directories (for .v and .vo files).
-Q _build/default/rocq-brick-libstdcpp/proof/ skylabs.brick.libstdcpp
-Q rocq-brick-libstdcpp/proof/ skylabs.brick.libstdcpp
-Q _build/default/rocq-brick-libstdcpp/test/ skylabs.brick.libstdcpp.test
-Q rocq-brick-libstdcpp/test/ skylabs.brick.libstdcpp.test