_CoqProject 1.74 KB
Newer Older
1
-Q theories iris_logrel
2
-arg -w -arg -notation-overridden,-redundant-canonical-projection,-several-object-files
3 4
theories/prelude/base.v
theories/prelude/hax.v
5
theories/prelude/bij.v
6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28
theories/F_mu_ref_conc/binder.v
theories/F_mu_ref_conc/lang.v
theories/F_mu_ref_conc/notation.v
theories/F_mu_ref_conc/subst.v
theories/F_mu_ref_conc/reflection.v
theories/F_mu_ref_conc/rules.v
theories/F_mu_ref_conc/typing.v
theories/F_mu_ref_conc/context_refinement.v
theories/F_mu_ref_conc/adequacy.v
theories/F_mu_ref_conc/pureexec.v
theories/F_mu_ref_conc/tactics.v
theories/logrel/threadpool.v
theories/logrel/rules_threadpool.v
theories/logrel/semtypes.v
theories/logrel/logrel_binary.v
theories/logrel/rules.v 
theories/logrel/proofmode/tactics_threadpool.v
theories/logrel/proofmode/tactics_rel.v
theories/logrel/fundamental_binary.v
theories/logrel/contextual_refinement.v
theories/logrel/soundness_binary.v
theories/logrel.v
theories/examples/lock.v
29
theories/examples/ticket_lock.v
30
theories/examples/bot.v
31 32 33 34 35 36 37
theories/examples/counter.v
theories/examples/lateearlychoice.v
theories/examples/par.v
theories/examples/bit.v
theories/examples/stack/CG_stack.v
theories/examples/stack/FG_stack.v
theories/examples/stack/refinement.v
38
theories/examples/stack/module_refinement.v
Dan Frumin's avatar
Dan Frumin committed
39 40
theories/examples/stack/mailbox.v
theories/examples/stack/helping.v
Dan Frumin's avatar
Dan Frumin committed
41
theories/examples/various.v
42
theories/examples/or.v
43
theories/examples/symbol.v
44
theories/examples/generative.v
45
theories/examples/Y.v
46
theories/examples/FAI.v
47
theories/examples/hospec/modular_counter.v
48
theories/examples/hospec/ticket_lock_refinement.v
Dan Frumin's avatar
Dan Frumin committed
49
theories/tests/typetest.v
Dan Frumin's avatar
Dan Frumin committed
50
theories/tests/ghosttp.v
Dan Frumin's avatar
Dan Frumin committed
51 52
theories/tests/tactics.v
theories/tests/tactics2.v
Dan Frumin's avatar
Dan Frumin committed
53 54
theories/tests/liftings.v
theories/tests/value.v
Dan Frumin's avatar
Dan Frumin committed
55
theories/examples/coqpl.v
56
theories/examples/brouwers.v