-
Notifications
You must be signed in to change notification settings - Fork 1
/
_CoqProject
132 lines (110 loc) · 4.27 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
-Q theories D
# We sometimes want to locally override notation (e.g. in proofmode/base.v, bi/embedding.v), and there
# is no good way to do that with scopes.
-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
# "Declare Scope" does not exist yet in 8.9.
# -arg -w -arg -undeclared-scope
# We have ambiguous paths and so far it is not even clear what they are (https://gitlab.mpi-sws.org/iris/iris/issues/240).
-arg -w -arg -ambiguous-paths
-arg -w -arg -deprecated-hint-rewrite-without-locality
-arg -w -arg -deprecated-instance-without-locality
-arg -w -arg -deprecated-typeclasses-transparency-without-locality
-arg -w -arg -future-coercion-class-field
theories/pure_program_logic/weakestpre.v
theories/pure_program_logic/lifting.v
theories/pure_program_logic/adequacy.v
theories/iris_extra/det_reduction.v
theories/iris_extra/cmra_prop_lift.v
theories/iris_extra/dlang.v
theories/iris_extra/iris_prelude.v
theories/iris_extra/lty.v
theories/iris_extra/persistence.v
theories/iris_extra/proofmode_extra.v
theories/iris_extra/pupd.v
theories/iris_extra/proofmode_pupd.v
theories/iris_extra/saved_interp_dep.v
theories/iris_extra/saved_interp_n.v
theories/iris_extra/swap_later_impl.v
theories/prelude.v
theories/asubst_intf.v
theories/asubst_base.v
theories/proper.v
theories/succ_notation.v
theories/numbers.v
theories/tactics.v
theories/Dot/syn/syn.v
theories/Dot/syn/rules.v
theories/Dot/syn/path_repl.v
theories/Dot/syn/path_repl_lemmas.v
theories/Dot/syn/lr_syn_aux.v
theories/Dot/syn/drop_skips.v
theories/Dot/syn/skeleton.v
theories/Dot/syn/core_stamping_defs.v
theories/Dot/syn/traversals.v
theories/Dot/lr/dlang_inst.v
theories/Dot/lr/dot_lty.v
theories/Dot/lr/path_wp.v
theories/Dot/lr/dot_semtypes.v
theories/Dot/lr/unary_lr.v
theories/Dot/lr/sem_unstamped_typing.v
theories/Dot/semtyp_lemmas/later_sub_sem.v
theories/Dot/semtyp_lemmas/binding_lr.v
theories/Dot/semtyp_lemmas/defs_lr.v
theories/Dot/semtyp_lemmas/dsub_lr.v
theories/Dot/semtyp_lemmas/path_repl_lr.v
theories/Dot/semtyp_lemmas/prims_lr.v
theories/Dot/semtyp_lemmas/tproj_lr.v
theories/Dot/syntyp_lemmas/binding_lr_syn.v
theories/Dot/syntyp_lemmas/dsub_lr_syn.v
theories/Dot/syntyp_lemmas/path_repl_lr_syn.v
theories/Dot/syntyp_lemmas/prims_lr_syn.v
theories/Dot/syntyp_lemmas/later_sub_syn.v
theories/Dot/typing/subtyping.v
theories/Dot/typing/type_eq.v
theories/Dot/typing/typing.v
theories/Dot/typing/typing_aux_defs.v
theories/Dot/fundamental.v
theories/Dot/examples/ex_utils.v
theories/Dot/examples/hoas.v
theories/Dot/examples/hoas_ex_utils.v
theories/Dot/examples/stamping/unstampedness_binding.v
theories/Dot/examples/old_typing/old_subtyping.v
theories/Dot/examples/old_typing/old_subtyping_derived_rules.v
theories/Dot/examples/old_typing/old_unstamped_typing.v
theories/Dot/examples/old_typing/old_unstamped_typing_derived_rules.v
theories/Dot/examples/old_typing/old_unstamped_typing_to_typing.v
theories/Dot/examples/old_fundamental.v
theories/Dot/examples/sem/semtyp_lemmas/sub_lr.v
theories/Dot/examples/sem/semtyp_lemmas/examples_lr.v
theories/Dot/examples/sem/syntyp_lemmas/sub_lr_syn.v
theories/Dot/examples/sem/syntyp_lemmas/examples_lr_syn.v
theories/Dot/examples/sem/ex_iris_utils.v
theories/Dot/examples/sem/no_russell_paradox.v
theories/Dot/examples/sem/prim_boolean_option.v
theories/Dot/examples/sem/storeless_typing.v
theories/Dot/examples/sem/storeless_typing_ex.v
theories/Dot/examples/sem/storeless_typing_ex_utils.v
theories/Dot/examples/sem/from_pdot_mutual_rec_sem.v
theories/Dot/examples/sem/small_sem_ex.v
theories/Dot/examples/sem/positive_div.v
theories/Dot/examples/syn/from_pdot_mutual_rec.v
theories/Dot/examples/syn/list.v
theories/Dot/examples/syn/old_unstamped_typing_ex.v
theories/Dot/examples/syn/scala_lib.v
theories/Dot/examples/syn/syn_lemmas.v
theories/Dot/hkdot/sem_kind.v
theories/Dot/hkdot/sem_kind_dot.v
theories/Dot/hkdot/hkdot.v
theories/DSub/syn/rules.v
theories/DSub/syn/syn.v
theories/DSub/syn/syn_lemmas.v
theories/DSub/lr/ty_interp_subst_lemmas.v
theories/DSub/lr/unary_lr.v
theories/DSub/lr/semtyp_lemmas.v
theories/DSub/typing/obj_ident_typing.v
theories/DSub/typing/storeless_typing.v
theories/DSub/fundamental.v