-
Notifications
You must be signed in to change notification settings - Fork 3
/
Copy pathCoqMakefile.conf
63 lines (52 loc) · 4.34 KB
/
CoqMakefile.conf
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
# This configuration file was generated by running:
# coq_makefile -f _CoqProject -o CoqMakefile
###############################################################################
# #
# Project files. #
# #
###############################################################################
COQMF_VFILES = Axiom/Meta.v Axiom/Extensionality.v Definition/Include.v Axiom/Separation.v Definition/RussellSet.v Definition/Emptyset.v Definition/Complement.v Axiom/Pairing.v Definition/Singleton.v Axiom/Union.v Definition/BinaryUnion.v Definition/TransitiveSet.v Axiom/Power.v Definition/OneTwo.v Definition/Successor.v Axiom/Infinity.v Definition/Omega.v Definition/EpsilonOrdering.v Theory/OrderingOnOmega.v Definition/Intersect.v Definition/BinaryIntersect.v Theory/BasicAlgebraOfSet.v Definition/OrderedPair.v Definition/Product.v Definition/Relation.v Definition/Function.v Lemma/MetaFunction.v Lemma/BasicFunction.v Axiom/Replacement.v Definition/Restriction.v Lemma/FunctionManeuver.v Definition/NatEmbedding.v Definition/OmegaRecursion.v Arith/Nat.v Notation/Class.v Theory/Ordinal.v Theory/OrdinalOperation.v Arith/Ord.v Arith/Tetration.v LargeOrdinals/LowerFixedPoint.v LargeOrdinals/EpsilonNumbers.v Example/Ch1_1.v Example/Ch1_2.v Example/Ch1_3.v Example/Ch1_4.v Example/Ch1_5.v Example/Ch1_6.v Example/Ch1_7.v Example/Ch1_8.v Example/Ch1_9.v Example/Ch1_10.v Example/Ch1_11.v Example/Ch1_12.v Example/Ch1_14.v Example/Ch1_15.v Example/Ch2_3.v Example/Ch2_4.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 . BBST
COQMF_COQLIBS_NOML = -R . BBST
COQMF_CMDLINE_COQLIBS =
###############################################################################
# #
# Coq configuration. #
# #
###############################################################################
COQMF_COQLIB=/Users/zhangqiuping/.opam/default/lib/coq/
COQMF_COQCORELIB=/Users/zhangqiuping/.opam/default/lib/coq/../coq-core//
COQMF_DOCDIR=/Users/zhangqiuping/.opam/default/doc/coq/
COQMF_OCAMLFIND=/Users/zhangqiuping/.opam/default/bin/ocamlfind
COQMF_CAMLFLAGS=-thread -rectypes -w +a-4-9-27-41-42-44-45-48-58-67-68-70 -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 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/ring plugins/rtauto plugins/ssr plugins/ssrmatching plugins/ssrsearch plugins/syntax
COQMF_COQ_NATIVE_COMPILER_DEFAULT=no
COQMF_WINDRIVE=
###############################################################################
# #
# Native compiler. #
# #
###############################################################################
COQMF_COQPROJECTNATIVEFLAG =
###############################################################################
# #
# Extra variables. #
# #
###############################################################################
COQMF_OTHERFLAGS =
COQMF_INSTALLCOQDOCROOT = BBST