_CoqProject 1008 Bytes
Newer Older
Robbert Krebbers's avatar
Robbert Krebbers committed
1
-Q theories iron
2
-arg -w -arg -notation-overridden,-redundant-canonical-projection,-several-object-files,-undeclared-scope,-convert_concl_no_check
Robbert Krebbers's avatar
Robbert Krebbers committed
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
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