-
Notifications
You must be signed in to change notification settings - Fork 0
/
_CoqProject
161 lines (160 loc) · 5.33 KB
/
_CoqProject
1
2
3
4
5
6
7
8
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
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
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
-Q theories lrust
# We sometimes want to locally override notation, and there is no good way to do that with scopes.
-arg -w -arg -notation-overridden
# Cannot use non-canonical projections as it causes massive unification failures
# (https://github.com/coq/coq/issues/6294).
-arg -w -arg -redundant-canonical-projection
theories/util/basic.v
theories/util/vector.v
theories/util/update.v
theories/util/discrete_fun.v
theories/util/fancy_lists.v
theories/util/pairwise.v
theories/util/list.v
theories/prophecy/syn_type.v
theories/prophecy/prophecy.v
theories/lifetime/model/definitions.v
theories/lifetime/model/faking.v
theories/lifetime/model/creation.v
theories/lifetime/model/primitive.v
theories/lifetime/model/accessors.v
theories/lifetime/model/borrow.v
theories/lifetime/model/borrow_sep.v
theories/lifetime/model/reborrow.v
theories/lifetime/lifetime_sig.v
theories/lifetime/lifetime.v
theories/lifetime/at_borrow.v
theories/lifetime/na_borrow.v
theories/lifetime/frac_borrow.v
theories/lang/adequacy.v
theories/lang/heap.v
theories/lang/time.v
theories/lang/lang.v
theories/lang/lifting.v
theories/lang/notation.v
theories/lang/proofmode.v
theories/lang/races.v
theories/lang/tactics.v
theories/lang/lib/memcpy.v
theories/lang/lib/swap.v
theories/lang/lib/new_delete.v
theories/lang/lib/spawn.v
theories/lang/lib/lock.v
theories/lang/lib/arc.v
theories/lang/lib/tests.v
theories/typing/base.v
theories/typing/uniq_cmra.v
theories/typing/type.v
theories/typing/lft_contexts.v
theories/typing/type_context.v
theories/typing/cont_context.v
theories/typing/uninit.v
theories/typing/base_type.v
theories/typing/mod_ty.v
theories/typing/refined.v
theories/typing/own.v
theories/typing/uniq_util.v
theories/typing/uniq_bor.v
theories/typing/shr_bor.v
theories/typing/product.v
theories/typing/product_split.v
theories/typing/sum.v
theories/typing/array_util.v
theories/typing/array.v
theories/typing/array_idx.v
theories/typing/bool.v
theories/typing/int.v
theories/typing/function.v
theories/typing/programs.v
theories/typing/borrow.v
theories/typing/cont.v
theories/typing/fixpoint.v
theories/typing/type_sum.v
theories/typing/zst.v
theories/typing/ghost.v
theories/typing/ghost_fn.v
theories/typing/hints.v
theories/typing/uniq_alt.v
theories/typing/uniq_alt_borrow.v
theories/typing/always_true.v
theories/typing/uniq_resolve.v
theories/typing/typing.v
theories/typing/soundness.v
theories/typing/uniq_array_util.v
theories/typing/ptr.v
theories/typing/lib/ghostptrtoken/heap_util.v
theories/typing/lib/ghostptrtoken/ghostseq.v
theories/typing/lib/ghostptrtoken/ghostseq_basic.v
theories/typing/lib/ghostptrtoken/permdata.v
theories/typing/lib/ghostptrtoken/permdata_basic.v
theories/typing/lib/ghostptrtoken/ghostptrtoken.v
theories/typing/lib/ghostptrtoken/ghostptrtoken_basic.v
theories/typing/lib/ghostptrtoken/ghostptrtoken_grow.v
theories/typing/lib/ghostptrtoken/ghostptrtoken_shrink_shr.v
theories/typing/lib/ghostptrtoken/ghostptrtoken_take_mut.v
theories/typing/lib/ghostptrtoken/ghostptrtoken_mut.v
theories/typing/lib/lib_ghost_fn.v
theories/typing/lib/ghostptrtoken/ghostptrtoken_index.v
theories/typing/lib/gfp.v
theories/typing/lib/panic.v
theories/typing/lib/loop.v
theories/typing/lib/option.v
theories/typing/lib/list.v
theories/typing/lib/maybe_uninit.v
theories/typing/lib/vec_util.v
theories/typing/lib/slice/slice.v
theories/typing/lib/slice/slice_basic.v
theories/typing/lib/slice/array_slice.v
theories/typing/lib/slice/slice_split.v
theories/typing/lib/slice/iter.v
theories/typing/lib/vec/vec.v
theories/typing/lib/vec/vec_basic.v
theories/typing/lib/vec/vec_slice.v
theories/typing/lib/vec/vec_index.v
theories/typing/lib/vec/vec_pushpop.v
theories/typing/lib/smallvec/smallvec.v
theories/typing/lib/smallvec/smallvec_basic.v
theories/typing/lib/smallvec/smallvec_slice.v
theories/typing/lib/smallvec/smallvec_index.v
theories/typing/lib/smallvec/smallvec_push.v
theories/typing/lib/smallvec/smallvec_pop.v
# theories/typing/lib/fake_shared.v
theories/typing/lib/cell.v
theories/typing/lib/spawn.v
# theories/typing/lib/join.v
# theories/typing/lib/take_mut.v
# theories/typing/lib/rc/rc.v
# theories/typing/lib/rc/weak.v
# theories/typing/lib/arc.v
theories/typing/lib/swap.v
# theories/typing/lib/diverging_static.v
theories/typing/lib/mutex/mutex.v
theories/typing/lib/mutex/mutexguard.v
# theories/typing/lib/refcell/refcell.v
# theories/typing/lib/refcell/ref.v
# theories/typing/lib/refcell/refmut.v
# theories/typing/lib/refcell/refcell_code.v
# theories/typing/lib/refcell/ref_code.v
# theories/typing/lib/refcell/refmut_code.v
# theories/typing/lib/rwlock/rwlock.v
# theories/typing/lib/rwlock/rwlockreadguard.v
# theories/typing/lib/rwlock/rwlockwriteguard.v
# theories/typing/lib/rwlock/rwlock_code.v
# theories/typing/lib/rwlock/rwlockreadguard_code.v
# theories/typing/lib/rwlock/rwlockwriteguard_code.v
theories/typing/examples/inc_max.v
theories/typing/examples/odd_sum.v
theories/typing/examples/projection_toggle.v
theories/typing/examples/take_some_list.v
theories/typing/examples/get_sum_list.v
theories/typing/examples/inc_some_list.v
theories/typing/examples/split_uniq_list.v
theories/typing/examples/inc_vec.v
theories/typing/examples/inc_cell.v
theories/typing/examples/get_x.v
theories/typing/examples/rebor.v
theories/typing/examples/unbox.v
theories/typing/examples/init_prod.v
theories/typing/examples/lazy_lft.v
# theories/typing/examples/nonlexical.v
theories/typing/examples/derived_rules.v