_CoqProject 1.15 KB
Newer Older
1
-Q . iris_logrel
2
-arg -w -arg -notation-overridden,-redundant-canonical-projection,-several-object-files
Amin Timany's avatar
Amin Timany committed
3
prelude/base.v
Amin Timany's avatar
Amin Timany committed
4
5
6
7
8
stlc/lang.v
stlc/typing.v
stlc/rules.v
stlc/logrel.v
stlc/fundamental.v
Amin Timany's avatar
Amin Timany committed
9
stlc/soundness.v
Amin Timany's avatar
Amin Timany committed
10
11
12
13
14
F_mu/lang.v
F_mu/typing.v
F_mu/rules.v
F_mu/logrel.v
F_mu/fundamental.v
Amin Timany's avatar
Amin Timany committed
15
F_mu/soundness.v
16
17
18
F_mu_ref/lang.v
F_mu_ref/typing.v
F_mu_ref/rules.v
19
F_mu_ref/rules_binary.v
20
F_mu_ref/logrel.v
21
F_mu_ref/logrel_binary.v
22
F_mu_ref/fundamental.v
23
F_mu_ref/fundamental_binary.v
Amin Timany's avatar
Amin Timany committed
24
F_mu_ref/soundness.v
25
26
F_mu_ref/context_refinement.v
F_mu_ref/soundness_binary.v
27
28
29
30
31
32
33
F_mu_ref_conc/lang.v
F_mu_ref_conc/rules.v
F_mu_ref_conc/typing.v
F_mu_ref_conc/logrel_unary.v
F_mu_ref_conc/fundamental_unary.v
F_mu_ref_conc/rules_binary.v
F_mu_ref_conc/logrel_binary.v
34
F_mu_ref_conc/weakestpre.v
35
36
37
38
F_mu_ref_conc/fundamental_binary.v
F_mu_ref_conc/soundness_unary.v
F_mu_ref_conc/context_refinement.v
F_mu_ref_conc/soundness_binary.v
39
F_mu_ref_conc/tactics.v
40
F_mu_ref_conc/notation.v
41
42
43
44
45
F_mu_ref_conc/examples/lock.v
F_mu_ref_conc/examples/counter.v
F_mu_ref_conc/examples/stack/stack_rules.v
F_mu_ref_conc/examples/stack/CG_stack.v
F_mu_ref_conc/examples/stack/FG_stack.v
46
F_mu_ref_conc/examples/stack/refinement.v