_CoqProject 1.43 KB
Newer Older
Robbert Krebbers's avatar
Robbert Krebbers committed
1
-Q theories iron
Ralf Jung's avatar
Ralf Jung committed
2 3 4 5 6 7 8 9 10 11 12
# "Declare Scope" does not exist yet in 8.9.
-arg -w -arg -undeclared-scope
# 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
# 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

Robbert Krebbers's avatar
Robbert Krebbers committed
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
theories/bi/fracpred.v
theories/proofmode/fracpred.v
theories/iron_logic/iron.v
theories/iron_logic/fcinv.v
theories/iron_logic/weakestpre.v
theories/iron_logic/adequacy.v
theories/iron_logic/lifting.v
theories/heap_lang/lang.v
theories/heap_lang/heap.v
theories/heap_lang/tactics.v
theories/heap_lang/lifting.v
theories/heap_lang/notation.v
theories/heap_lang/adequacy.v
theories/heap_lang/proofmode.v
theories/heap_lang/lib/spawn.v
theories/heap_lang/lib/par.v
theories/heap_lang/lib/spin_lock.v
theories/heap_lang/lib/spin_lock_track.v
theories/heap_lang/lib/resource_transfer_par.v
theories/heap_lang/lib/resource_transfer_fork.v
theories/heap_lang/lib/resource_transfer_sts.v
theories/heap_lang/lib/list.v
theories/heap_lang/lib/bag.v
theories/heap_lang/lib/queue.v
theories/heap_lang/lib/message_passing.v
theories/heap_lang/lib/message_passing_example.v