_CoqProject 4.07 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
14

15
theories/lecture_notes/coq_intro_example_1.v
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

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
91
theories/hocap/concurrent_runners.v
92
theories/hocap/parfib.v
93

94
theories/logatom/lib/gc.v
95
theories/logatom/treiber.v
96
theories/logatom/treiber2.v
97
theories/logatom/elimination_stack/hocap_spec.v
98 99
theories/logatom/elimination_stack/stack.v
theories/logatom/elimination_stack/spec.v
100 101 102 103 104 105
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
106 107
theories/logatom/snapshot/spec.v
theories/logatom/snapshot/atomic_snapshot.v
108 109
theories/logatom/conditional_increment/spec.v
theories/logatom/conditional_increment/cinc.v
110 111
theories/logatom/rdcss/rdcss.v
theories/logatom/rdcss/spec.v
Amin Timany's avatar
Amin Timany committed
112
theories/logatom/proph_erasure.v
113 114
theories/logatom/herlihy_wing_queue/spec.v
theories/logatom/herlihy_wing_queue/hwq.v