-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy path_CoqProject
92 lines (90 loc) · 5.22 KB
/
_CoqProject
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
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
# Warns about entries in this _CoqProject
-arg -w -arg -cannot-open-path
# Warnings from `dune`
-arg -w -arg -notation-overridden
-arg -w -arg -custom-entry-overridden
-arg -w -arg -redundant-canonical-projection
-arg -w -arg -ambiguous-paths
# 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
# Plugin directory.
-I _build/install/default/lib
# Specified logical paths for directories (for .v and .vo files).
-Q fmdeps/coq/user-contrib/Ltac2 Ltac2
-Q _build/default/fmdeps/coq/user-contrib/Ltac2 Ltac2
-Q fmdeps/coq-ext-lib/theories/ ExtLib
-Q _build/default/fmdeps/coq-ext-lib/theories/ ExtLib
-Q fmdeps/coq-equations/theories/ Equations
-Q _build/default/fmdeps/coq-equations/theories/ Equations
-Q fmdeps/coq-elpi/theories/ elpi
-Q _build/default/fmdeps/coq-elpi/theories/ elpi
-Q _build/default/fmdeps/coq-elpi/elpi/ elpi_elpi
-Q fmdeps/coq-elpi/apps/NES/theories/ elpi.apps.NES
-Q _build/default/fmdeps/coq-elpi/apps/NES/theories/ elpi.apps.NES
-Q _build/default/fmdeps/coq-elpi/apps/NES/elpi/ elpi.apps.NES.elpi
-Q fmdeps/coq-elpi/apps/derive/theories/ elpi.apps.derive
-Q _build/default/fmdeps/coq-elpi/apps/derive/theories/ elpi.apps.derive
-Q _build/default/fmdeps/coq-elpi/apps/derive/elpi/ elpi.apps.derive.elpi
-Q fmdeps/coq-elpi/apps/locker/theories/ elpi.apps.locker
-Q _build/default/fmdeps/coq-elpi/apps/locker/theories/ elpi.apps.locker
-Q _build/default/fmdeps/coq-elpi/apps/locker/elpi/ elpi.apps.locker.elpi
-Q fmdeps/stdpp/stdpp/ stdpp
-Q _build/default/fmdeps/stdpp/stdpp/ stdpp
-Q fmdeps/stdpp/stdpp_bitvector/ stdpp.bitvector
-Q _build/default/fmdeps/stdpp/stdpp_bitvector/ stdpp.bitvector
-Q fmdeps/stdpp/stdpp_unstable/ stdpp.unstable
-Q _build/default/fmdeps/stdpp/stdpp_unstable/ stdpp.unstable
-Q fmdeps/iris/iris/ iris
-Q _build/default/fmdeps/iris/iris/ iris
-Q fmdeps/iris/iris_heap_lang/ iris.heap_lang
-Q _build/default/fmdeps/iris/iris_heap_lang/ iris.heap_lang
-Q fmdeps/iris/iris_unstable/ iris.unstable
-Q _build/default/fmdeps/iris/iris_unstable/ iris.unstable
-Q fmdeps/iris/iris_deprecated/ iris.deprecated
-Q _build/default/fmdeps/iris/iris_deprecated/ iris.deprecated
-Q fmdeps/cpp2v-core/rocq-bluerock-brick/theories/prelude/ bedrock.prelude
-Q _build/default/fmdeps/cpp2v-core/rocq-bluerock-brick/theories/prelude/ bedrock.prelude
-Q fmdeps/cpp2v-core/rocq-bluerock-brick/theories/lang/ bedrock.lang
-Q _build/default/fmdeps/cpp2v-core/rocq-bluerock-brick/theories/lang/ bedrock.lang
-Q fmdeps/cpp2v-core/rocq-bluerock-brick/theories/noimport/ bedrock.noimport
-Q _build/default/fmdeps/cpp2v-core/rocq-bluerock-brick/theories/noimport/ bedrock.noimport
-Q fmdeps/cpp2v-core/rocq-lens/Lens/ Lens
-Q _build/default/fmdeps/cpp2v-core/rocq-lens/Lens/ Lens
-Q fmdeps/cpp2v-core/rocq-upoly/upoly/ bedrock.upoly
-Q _build/default/fmdeps/cpp2v-core/rocq-upoly/upoly/ bedrock.upoly
-Q fmdeps/cpp2v-core/rocq-bluerock-brick/tests/ bedrocktest
-Q _build/default/fmdeps/cpp2v-core/rocq-bluerock-brick/tests/ bedrocktest
-Q fmdeps/cpp2v-core/ltac2-extra/theories/ bedrock.ltac2.extra
-Q _build/default/fmdeps/cpp2v-core/ltac2-extra/theories/ bedrock.ltac2.extra
-Q fmdeps/cpp2v-core/ltac2-extra/tests/ bedrock_tests.ltac2.extra
-Q _build/default/fmdeps/cpp2v-core/ltac2-extra/tests/ bedrock_tests.ltac2.extra
-Q fmdeps/cpp2v-core/ltac2-logger/theories/ bedrock.ltac2.logger
-Q _build/default/fmdeps/cpp2v-core/ltac2-logger/theories/ bedrock.ltac2.logger
-Q fmdeps/cpp2v-core/elpi-extra/extra/ bedrock.elpi.extra
-Q _build/default/fmdeps/cpp2v-core/elpi-extra/extra/ bedrock.elpi.extra
-Q fmdeps/cpp2v/coq-bluerock-auto-core/theories/ bedrock.auto.core
-Q _build/default/fmdeps/cpp2v/coq-bluerock-auto-core/theories/ bedrock.auto.core
-Q fmdeps/cpp2v/coq-bluerock-auto-core/examples/ bedrock_auto_core.examples
-Q _build/default/fmdeps/cpp2v/coq-bluerock-auto-core/examples/ bedrock_auto_core.examples
-Q fmdeps/cpp2v/coq-bluerock-auto-core/tests/ bedrock_auto_core.tests
-Q _build/default/fmdeps/cpp2v/coq-bluerock-auto-core/tests/ bedrock_auto_core.tests
-Q fmdeps/cpp2v/coq-bluerock-auto-cpp/theories/ bedrock
-Q _build/default/fmdeps/cpp2v/coq-bluerock-auto-cpp/theories/ bedrock
-Q fmdeps/cpp2v/coq-bluerock-auto-cpp/tests/ bedrock_auto.tests
-Q _build/default/fmdeps/cpp2v/coq-bluerock-auto-cpp/tests/ bedrock_auto.tests
-Q fmdeps/cpp2v/coq-bluerock-hw-models/theories/ bedrock.hw_models
-Q _build/default/fmdeps/cpp2v/coq-bluerock-hw-models/theories/ bedrock.hw_models
-Q fmdeps/cpp2v/coq-bluerock-hw-models-extra/theories/ bedrock.hw_models
-Q _build/default/fmdeps/cpp2v/coq-bluerock-hw-models-extra/theories/ bedrock.hw_models
-Q fmdeps/cpp2v/coq-bluerock-nova-interface/theories/ bedrock.nova_interface
-Q _build/default/fmdeps/cpp2v/coq-bluerock-nova-interface/theories/ bedrock.nova_interface
-Q fmdeps/cpp2v/coq-bluerock-lts-adequacy/theories/ bedrock.lts_adequacy_demo
-Q _build/default/fmdeps/cpp2v/coq-bluerock-lts-adequacy/theories/ bedrock.lts_adequacy_demo
-Q fmdeps/cpp2v/elpi-cpp/cpp/ bedrock.elpi.cpp
-Q _build/default/fmdeps/cpp2v/elpi-cpp/cpp/ bedrock.elpi.cpp
-Q fmdeps/cpp2v/elpi-cpp/tests/ bedrock_tests.elpi.cpp
-Q _build/default/fmdeps/cpp2v/elpi-cpp/tests/ bedrock_tests.elpi.cpp