_CoqProject 2.11 KB
Newer Older
Ralf Jung's avatar
Ralf Jung committed
1 2 3 4 5 6
-Q theories iris_examples
-arg -w -arg -notation-overridden,-redundant-canonical-projection,-several-object-files
theories/barrier/proof.v
theories/barrier/specification.v
theories/barrier/barrier.v
theories/barrier/protocol.v
Ralf Jung's avatar
Ralf Jung committed
7
theories/barrier/example_client.v
Ralf Jung's avatar
Ralf Jung committed
8
theories/barrier/example_joining_existentials.v
Amin Timany's avatar
Amin Timany committed
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

theories/iris_logrel/prelude/base.v
theories/iris_logrel/stlc/lang.v
theories/iris_logrel/stlc/typing.v
theories/iris_logrel/stlc/rules.v
theories/iris_logrel/stlc/logrel.v
theories/iris_logrel/stlc/fundamental.v
theories/iris_logrel/stlc/soundness.v
theories/iris_logrel/F_mu/lang.v
theories/iris_logrel/F_mu/typing.v
theories/iris_logrel/F_mu/rules.v
theories/iris_logrel/F_mu/logrel.v
theories/iris_logrel/F_mu/fundamental.v
theories/iris_logrel/F_mu/soundness.v
theories/iris_logrel/F_mu_ref/lang.v
theories/iris_logrel/F_mu_ref/typing.v
theories/iris_logrel/F_mu_ref/rules.v
theories/iris_logrel/F_mu_ref/rules_binary.v
theories/iris_logrel/F_mu_ref/logrel.v
theories/iris_logrel/F_mu_ref/logrel_binary.v
theories/iris_logrel/F_mu_ref/fundamental.v
theories/iris_logrel/F_mu_ref/fundamental_binary.v
theories/iris_logrel/F_mu_ref/soundness.v
theories/iris_logrel/F_mu_ref/context_refinement.v
theories/iris_logrel/F_mu_ref/soundness_binary.v
theories/iris_logrel/F_mu_ref_conc/lang.v
theories/iris_logrel/F_mu_ref_conc/rules.v
theories/iris_logrel/F_mu_ref_conc/typing.v
theories/iris_logrel/F_mu_ref_conc/logrel_unary.v
theories/iris_logrel/F_mu_ref_conc/fundamental_unary.v
theories/iris_logrel/F_mu_ref_conc/rules_binary.v
theories/iris_logrel/F_mu_ref_conc/logrel_binary.v
theories/iris_logrel/F_mu_ref_conc/fundamental_binary.v
theories/iris_logrel/F_mu_ref_conc/soundness_unary.v
theories/iris_logrel/F_mu_ref_conc/context_refinement.v
theories/iris_logrel/F_mu_ref_conc/soundness_binary.v
theories/iris_logrel/F_mu_ref_conc/examples/lock.v
theories/iris_logrel/F_mu_ref_conc/examples/counter.v
theories/iris_logrel/F_mu_ref_conc/examples/stack/stack_rules.v
theories/iris_logrel/F_mu_ref_conc/examples/stack/CG_stack.v
theories/iris_logrel/F_mu_ref_conc/examples/stack/FG_stack.v
theories/iris_logrel/F_mu_ref_conc/examples/stack/refinement.v