_CoqProject 3.78 KB
Newer Older
Ralf Jung's avatar
Ralf Jung committed
1
-Q theories iris_examples
Ralf Jung's avatar
Ralf Jung committed
2
# We sometimes want to locally override notation and there is no good way to do that with scopes.
Ralf Jung's avatar
Ralf Jung committed
3 4 5 6 7 8
-arg -w -arg -notation-overridden
# non-canonical projections (https://github.com/coq/coq/pull/10076) do not exist yet in 8.9.
-arg -w -arg -redundant-canonical-projection
# change_no_check does not exist yet in 8.9.
-arg -w -arg -convert_concl_no_check

Ralf Jung's avatar
Ralf Jung committed
9 10 11
theories/barrier/proof.v
theories/barrier/specification.v
theories/barrier/barrier.v
Ralf Jung's avatar
Ralf Jung committed
12
theories/barrier/example_client.v
Ralf Jung's avatar
Ralf Jung committed
13
theories/barrier/example_joining_existentials.v
Amin Timany's avatar
Amin Timany committed
14

15
theories/lecture_notes/coq_intro_example_1.v
Ralf Jung's avatar
Ralf Jung committed
16
theories/lecture_notes/coq_intro_example_2.v
17 18 19 20 21 22 23 24
theories/lecture_notes/lists.v
theories/lecture_notes/lists_guarded.v
theories/lecture_notes/lock.v
theories/lecture_notes/lock_unary_spec.v
theories/lecture_notes/modular_incr.v
theories/lecture_notes/recursion_through_the_store.v
theories/lecture_notes/stack.v
theories/lecture_notes/ccounter.v
25 26 27 28 29 30

theories/spanning_tree/graph.v
theories/spanning_tree/mon.v
theories/spanning_tree/spanning.v
theories/spanning_tree/proof.v

Daniel Gratzer's avatar
Daniel Gratzer committed
31
theories/concurrent_stacks/specs.v
32
theories/concurrent_stacks/concurrent_stack1.v
33
theories/concurrent_stacks/concurrent_stack2.v
34
theories/concurrent_stacks/concurrent_stack3.v
35
theories/concurrent_stacks/concurrent_stack4.v
36

Amin Timany's avatar
Amin Timany committed
37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76
theories/logrel/prelude/base.v
theories/logrel/stlc/lang.v
theories/logrel/stlc/typing.v
theories/logrel/stlc/rules.v
theories/logrel/stlc/logrel.v
theories/logrel/stlc/fundamental.v
theories/logrel/stlc/soundness.v
theories/logrel/F_mu/lang.v
theories/logrel/F_mu/typing.v
theories/logrel/F_mu/rules.v
theories/logrel/F_mu/logrel.v
theories/logrel/F_mu/fundamental.v
theories/logrel/F_mu/soundness.v
theories/logrel/F_mu_ref/lang.v
theories/logrel/F_mu_ref/typing.v
theories/logrel/F_mu_ref/rules.v
theories/logrel/F_mu_ref/rules_binary.v
theories/logrel/F_mu_ref/logrel.v
theories/logrel/F_mu_ref/logrel_binary.v
theories/logrel/F_mu_ref/fundamental.v
theories/logrel/F_mu_ref/fundamental_binary.v
theories/logrel/F_mu_ref/soundness.v
theories/logrel/F_mu_ref/context_refinement.v
theories/logrel/F_mu_ref/soundness_binary.v
theories/logrel/F_mu_ref_conc/lang.v
theories/logrel/F_mu_ref_conc/rules.v
theories/logrel/F_mu_ref_conc/typing.v
theories/logrel/F_mu_ref_conc/logrel_unary.v
theories/logrel/F_mu_ref_conc/fundamental_unary.v
theories/logrel/F_mu_ref_conc/rules_binary.v
theories/logrel/F_mu_ref_conc/logrel_binary.v
theories/logrel/F_mu_ref_conc/fundamental_binary.v
theories/logrel/F_mu_ref_conc/soundness_unary.v
theories/logrel/F_mu_ref_conc/context_refinement.v
theories/logrel/F_mu_ref_conc/soundness_binary.v
theories/logrel/F_mu_ref_conc/examples/lock.v
theories/logrel/F_mu_ref_conc/examples/counter.v
theories/logrel/F_mu_ref_conc/examples/stack/stack_rules.v
theories/logrel/F_mu_ref_conc/examples/stack/CG_stack.v
theories/logrel/F_mu_ref_conc/examples/stack/FG_stack.v
Ralf Jung's avatar
Ralf Jung committed
77
theories/logrel/F_mu_ref_conc/examples/stack/refinement.v
78
theories/logrel/F_mu_ref_conc/examples/fact.v
79

80 81 82 83
theories/logrel_heaplang/ltyping.v
theories/logrel_heaplang/ltyping_safety.v
theories/logrel_heaplang/lib/symbol_adt.v

84 85
theories/hocap/abstract_bag.v
theories/hocap/cg_bag.v
86
theories/hocap/fg_bag.v
87 88
theories/hocap/exclusive_bag.v
theories/hocap/shared_bag.v
Dan Frumin's avatar
Dan Frumin committed
89
theories/hocap/contrib_bag.v
90
theories/hocap/lib/oneshot.v
Dan Frumin's avatar
Dan Frumin committed
91
theories/hocap/concurrent_runners.v
92
theories/hocap/parfib.v
93

94
theories/logatom/treiber.v
95
theories/logatom/treiber2.v
96
theories/logatom/elimination_stack/hocap_spec.v
97 98
theories/logatom/elimination_stack/stack.v
theories/logatom/elimination_stack/spec.v
99 100 101 102 103 104
theories/logatom/flat_combiner/flat.v
theories/logatom/flat_combiner/simple_sync.v
theories/logatom/flat_combiner/sync.v
theories/logatom/flat_combiner/peritem.v
theories/logatom/flat_combiner/atomic_sync.v
theories/logatom/flat_combiner/misc.v
105 106
theories/logatom/snapshot/spec.v
theories/logatom/snapshot/atomic_snapshot.v