-
Notifications
You must be signed in to change notification settings - Fork 2
Expand file tree
/
Copy path_CoqProject
More file actions
68 lines (65 loc) · 2.33 KB
/
Copy path_CoqProject
File metadata and controls
68 lines (65 loc) · 2.33 KB
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
-Q theories cgraphs
# 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
-arg -w -arg -cannot-define-projection
# 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 -native-compiler -arg no
theories/cgraphs/multiset.v
theories/cgraphs/util.v
theories/cgraphs/mapexcl.v
theories/cgraphs/uforests.v
theories/cgraphs/upred.v
theories/cgraphs/bi.v
theories/cgraphs/seplogic.v
theories/cgraphs/cgraph.v
theories/cgraphs/genericinv.v
# theories/sessiontypes/langdef.v
# theories/sessiontypes/rtypesystem.v
# theories/sessiontypes/invariant.v
# theories/sessiontypes/progress.v
# theories/sessiontypes/safety.v
# theories/sessiontypes/ycombinator.v
#
# theories/multiparty/mutil.v
# theories/multiparty/langdef.v
# theories/multiparty/definitions.v
# theories/multiparty/rtypesystem.v
# theories/multiparty/invariant.v
# theories/multiparty/progress.v
# theories/multiparty/ycombinator.v
# theories/multiparty/globaltypes.v
# theories/multiparty/binary.v
# theories/multiparty/theorems.v
#
# theories/lambdabar/langtools.v
# theories/lambdabar/langdef.v
# theories/lambdabar/definitions.v
# theories/lambdabar/rtypesystem.v
# theories/lambdabar/invariant.v
# theories/lambdabar/theorems.v
# theories/lambdabar/sessions.v
# theories/lambdabar/letmacro.v
# theories/lambdabar/compiler.v
# theories/locks/lambdalock/langtools.v
# theories/locks/lambdalock/langdef.v
# theories/locks/lambdalock/definitions.v
# theories/locks/lambdalock/rtypesystem.v
# theories/locks/lambdalock/invariant.v
# theories/locks/lambdalock/theorems.v
# theories/locks/lambdalock/letmacro.v
#
# theories/locks/lambdalockpp/langtools.v
# theories/locks/lambdalockpp/langdef.v
# theories/locks/lambdalockpp/definitions.v
# theories/locks/lambdalockpp/rtypesystem.v
# theories/locks/lambdalockpp/invariant.v
# theories/locks/lambdalockpp/theorems.v
# theories/locks/lambdalockpp/letmacro.v