-
Notifications
You must be signed in to change notification settings - Fork 4
Expand file tree
/
Copy pathCoqMakefile.conf
More file actions
55 lines (46 loc) · 4.19 KB
/
Copy pathCoqMakefile.conf
File metadata and controls
55 lines (46 loc) · 4.19 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
# This configuration file was generated by running:
# coq_makefile -f _CoqProject -o CoqMakefile
###############################################################################
# #
# Project files. #
# #
###############################################################################
COQMF_VFILES = Axiom/Meta.v Axiom/ZFC0.v Axiom/ZFC1.v Axiom/ZFC2.v Axiom/ZFC3.v Lib/Essential.v Lib/EpsilonInduction.v Lib/EpsilonImpliesAC.v Lib/Class.v Elements/EST2.v Elements/EX2.v Elements/EST3_1.v Elements/EST3_2.v Elements/EST3_3.v Elements/EX3_1.v Elements/EX3_2.v Elements/EST7_1.v Lib/Relation.v Lib/FuncFacts.v Elements/EST4_1.v Elements/EST4_2.v Elements/EST4_3.v Elements/EX4.v Lib/Natural.v Lib/NatIsomorphism.v Lib/WosetMin.v Elements/EST5_1.v Elements/EST5_2.v Elements/EST5_3.v Elements/EST5_4.v Elements/EX5.v Elements/EST5_5.v Elements/EST5_6.v Elements/EST5_7.v Lib/Real.v Elements/EST6_1.v Lib/Algebra/Inj_2n3m.v Lib/IndexedFamilyUnion.v Lib/Dominate.v Lib/ChoiceFacts.v Lib/Choice.v Elements/EST7_2.v Elements/EST7_3.v Elements/EST7_4.v Elements/EST7_5.v Elements/EST6_2.v Elements/EX6_1.v Lib/NaturalFacts.v Lib/OrdFacts.v Elements/EST6_3.v Elements/EST6_4.v Elements/EX6_2.v Elements/EST6_5.v Elements/EST6_6.v Elements/EX6_3.v Lib/Cardinal.v Elements/EX7_1.v Elements/EX7_2.v Lib/Ordinal.v Lib/ZornsLemma.v Elements/EST7_6.v Lib/ScottsTrick.v Elements/EX7_3.v Lib/LoStruct.v Lib/WoStructExtension.v Elements/EST8_1.v Elements/EST8_2.v Elements/EST8_3.v Elements/EST8_4.v Elements/EX8_1.v Elements/EX8_2.v Elements/EX8_3.v Elements/EX8_4.v Elements/EST8_5.v Elements/EST8_6.v Elements/EST8_7.v LargeOrdinals/OrdinalCountability.v LargeOrdinals/SidedTetration.v LargeOrdinals/EpsilonNumbers.v LargeOrdinals/LowerFixedPoint.v LargeOrdinals/GeneralEpsilon.v LargeOrdinals/NormalTetration.v
COQMF_MLIFILES =
COQMF_MLFILES =
COQMF_MLGFILES =
COQMF_MLPACKFILES =
COQMF_MLLIBFILES =
COQMF_CMDLINE_VFILES =
###############################################################################
# #
# Path directives (-I, -R, -Q). #
# #
###############################################################################
COQMF_OCAMLLIBS =
COQMF_SRC_SUBDIRS =
COQMF_COQLIBS = -R . ZFC
COQMF_COQLIBS_NOML = -R . ZFC
COQMF_CMDLINE_COQLIBS =
###############################################################################
# #
# Coq configuration. #
# #
###############################################################################
COQMF_LOCAL=0
COQMF_COQLIB=/usr/local/lib/coq/
COQMF_DOCDIR=/usr/local/Cellar/coq/8.13.2/share/doc/coq/
COQMF_OCAMLFIND=/usr/local/opt/ocaml-findlib/bin/ocamlfind
COQMF_CAMLFLAGS=-thread -rectypes -w +a-4-9-27-41-42-44-45-48-58-67 -safe-string -strict-sequence
COQMF_WARN=-warn-error +a-3
COQMF_HASNATDYNLINK=true
COQMF_COQ_SRC_SUBDIRS=config lib clib kernel library engine pretyping interp gramlib gramlib/.pack parsing proofs tactics toplevel printing ide stm vernac plugins/btauto plugins/cc plugins/derive plugins/extraction plugins/firstorder plugins/funind plugins/ltac plugins/micromega plugins/nsatz plugins/omega plugins/ring plugins/rtauto plugins/ssr plugins/ssrmatching plugins/ssrsearch plugins/syntax
COQMF_COQ_NATIVE_COMPILER_DEFAULT=ondemand
COQMF_WINDRIVE=
###############################################################################
# #
# Extra variables. #
# #
###############################################################################
COQMF_OTHERFLAGS =
COQMF_INSTALLCOQDOCROOT = ZFC