-
Notifications
You must be signed in to change notification settings - Fork 7
/
Copy path_CoqProject
89 lines (72 loc) · 2.2 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
-docroot .
-arg -w -arg -notation-overridden
COQDOCFLAGS = "--charset utf-8 -s --with-header ../website/resources/header.html --with-footer ../website/resources/footer.html --index indexpage --external https://uds-psl.github.io/coq-library-fol/undec Undecidability"
-Q . FOL
# Warning seems incorrect, see https://github.com/coq/coq/issues/19631
# Disabled for now to reduce spam.
-arg -w -arg -notation-incompatible-prefix
# Disable warnings about vectors being hard to use. We know how to work with them.
-arg -w -arg -warn-library-file-stdlib-vector
FullSyntax.v
FragmentSyntax.v
Arithmetics.v
Theories.v
Sets.v
FiniteSets.v
Semantics/Heyting/Heyting.v
Semantics/Heyting/Soundness.v
Deduction/FragmentSequent.v
Deduction/FragmentSequentFacts.v
Deduction/FullSequent.v
Deduction/FullSequentFacts.v
Utils/PrenexNormalForm.v
Utils/MPFacts.v
ArithmeticalHierarchy/ArithmeticalHierarchySyntactic.v
ArithmeticalHierarchy/ArithmeticalHierarchySemantic.v
ArithmeticalHierarchy/ArithmeticalHierarchyEquiv.v
Completeness/TarskiConstructions.v
Completeness/Consistency.v
Completeness/EnumerationUtils.v
Completeness/TarskiCompleteness.v
Completeness/KripkeCompleteness.v
Completeness/HeytingMacNeille.v
Completeness/HeytingCompleteness.v
Reification/GeneralReflection.v
Reification/DemoPA.v
Reification/DemoPAExtensional.v
Proofmode/StringToIdent.v
Proofmode/Hoas.v
Proofmode/Theories.v
Proofmode/ProofMode.v
Proofmode/DemoPA.v
Proofmode/DemoZF.v
Proofmode/DemoMinZF.v
Incompleteness/Abstract.v
Incompleteness/Axiomatisations.v
Incompleteness/PA_incompleteness.v
Incompleteness/utils.v
Incompleteness/epf.v
Incompleteness/epf_mu.v
Incompleteness/formal_systems.v
Incompleteness/abstract_incompleteness.v
Incompleteness/fol_utils.v
Incompleteness/qdec.v
Incompleteness/sigma1.v
Incompleteness/bin_qdec.v
Incompleteness/weak_strong.v
Incompleteness/ctq.v
Incompleteness/fol_incompleteness.v
Tennenbaum/SyntheticInType.v
Tennenbaum/NumberUtils.v
Tennenbaum/DN_Utils.v
Tennenbaum/MoreDecidabilityFacts.v
Tennenbaum/Peano.v
Tennenbaum/Formulas.v
Tennenbaum/Church.v
Tennenbaum/CantorPairing.v
Tennenbaum/Coding.v
Tennenbaum/Tennenbaum_diagonal.v
Tennenbaum/Tennenbaum_insep.v
Tennenbaum/HA_insep.v
Tennenbaum/Variants.v
Tennenbaum/Abstract_coding.v