_CoqProject 1.17 KB
Newer Older
1
-Q theories iris_c
2 3 4 5 6 7 8 9
# We sometimes want to locally override notation and there is no good way to do that with scopes.
-arg -w -arg -notation-overridden
# non-canonical projections (https://github.com/coq/coq/pull/10076) do not exist yet in 8.9.
-arg -w -arg -redundant-canonical-projection
# change_no_check does not exist yet in 8.9.
-arg -w -arg -convert_concl_no_check
# "Declare Scope" does not exist yet in 8.9.
-arg -w -arg -undeclared-scope
10 11
# We have ambiguous paths and so far it is not even clear what they are (https://gitlab.mpi-sws.org/iris/iris/issues/240).
-arg -w -arg -ambiguous-paths
12

13
theories/lib/list.v
14
theories/lib/mset.v
15
theories/lib/flock.v
16
theories/lib/locking_heap.v
Dan Frumin's avatar
Dan Frumin committed
17
theories/lib/U.v
Robbert Krebbers's avatar
Robbert Krebbers committed
18
theories/lib/Q.v
19
theories/c_translation/monad.v
Dan Frumin's avatar
Dan Frumin committed
20
theories/c_translation/proofmode.v
21
theories/c_translation/translation.v
22
theories/vcgen/dcexpr.v
Léon Gondelman's avatar
Léon Gondelman committed
23
theories/vcgen/denv.v
24
theories/vcgen/forward.v
Léon Gondelman 's avatar
Léon Gondelman committed
25
theories/vcgen/vcg.v
Robbert Krebbers's avatar
Robbert Krebbers committed
26
theories/vcgen/reification.v
Léon Gondelman 's avatar
Léon Gondelman committed
27
theories/vcgen/proofmode.v
28 29 30 31 32
theories/tests/basics.v
theories/tests/invoke.v
theories/tests/unknowns.v
theories/tests/swap.v
theories/tests/fact.v
Robbert Krebbers's avatar
Robbert Krebbers committed
33
theories/tests/array_copy.v
34
theories/tests/gcd.v
Robbert Krebbers's avatar
Robbert Krebbers committed
35
theories/tests/par_inc.v
36
theories/tests/store_strong.v