_CoqProject 1 KB
Newer Older
1
-Q . iris_logrel
2
-arg -w -arg -notation-overridden,-redundant-canonical-projection,-several-object-files
Dan Frumin's avatar
Dan Frumin committed
3
prelude/ds.v
4
prelude/base.v
5
F_mu_ref_conc/binder.v
6
F_mu_ref_conc/lang.v
7
F_mu_ref_conc/subst.v
8
F_mu_ref_conc/hax.v
9
F_mu_ref_conc/reflection.v
10 11
F_mu_ref_conc/rules.v
F_mu_ref_conc/typing.v
12 13
# F_mu_ref_conc/logrel_unary.v
# F_mu_ref_conc/fundamental_unary.v
14
F_mu_ref_conc/relational_properties.v
15 16 17
F_mu_ref_conc/rules_binary.v
F_mu_ref_conc/logrel_binary.v
F_mu_ref_conc/fundamental_binary.v
18
# F_mu_ref_conc/soundness_unary.v
19
F_mu_ref_conc/context_refinement.v
20
F_mu_ref_conc/adequacy.v
21
F_mu_ref_conc/soundness_binary.v
22
F_mu_ref_conc/tactics.v
23
F_mu_ref_conc/rel_tactics.v
24
F_mu_ref_conc/notation.v
25 26
F_mu_ref_conc/examples/lock.v
F_mu_ref_conc/examples/counter.v
27
F_mu_ref_conc/examples/lateearlychoice.v
28
F_mu_ref_conc/examples/par.v
Dan Frumin's avatar
Dan Frumin committed
29
F_mu_ref_conc/examples/bit.v
30 31 32 33
#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
#F_mu_ref_conc/examples/stack/refinement.v