_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