-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathMakefile.conf
58 lines (49 loc) · 3.95 KB
/
Makefile.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
# This configuration file was generated by running:
# coq_makefile OTHERFLAGS = '' COQLIBS = '' -install none Preface.v Basics.v Induction.v Lists.v Poly.v Tactics.v Logic.v IndProp.v Maps.v ProofObjects.v IndPrinciples.v Rel.v Imp.v ImpParser.v ImpCEvalFun.v Extraction.v Auto.v Postscript.v Bib.v PrefaceTest.v BasicsTest.v InductionTest.v ListsTest.v PolyTest.v TacticsTest.v LogicTest.v IndPropTest.v MapsTest.v ProofObjectsTest.v IndPrinciplesTest.v RelTest.v ImpTest.v ImpParserTest.v ImpCEvalFunTest.v ExtractionTest.v AutoTest.v PostscriptTest.v BibTest.v -o Makefile
###############################################################################
# #
# Project files. #
# #
###############################################################################
COQMF_VFILES = Preface.v Basics.v Induction.v Lists.v Poly.v Tactics.v Logic.v IndProp.v Maps.v ProofObjects.v IndPrinciples.v Rel.v Imp.v ImpParser.v ImpCEvalFun.v Extraction.v Auto.v Postscript.v Bib.v PrefaceTest.v BasicsTest.v InductionTest.v ListsTest.v PolyTest.v TacticsTest.v LogicTest.v IndPropTest.v MapsTest.v ProofObjectsTest.v IndPrinciplesTest.v RelTest.v ImpTest.v ImpParserTest.v ImpCEvalFunTest.v ExtractionTest.v AutoTest.v PostscriptTest.v BibTest.v
COQMF_MLIFILES =
COQMF_MLFILES =
COQMF_ML4FILES =
COQMF_MLPACKFILES =
COQMF_MLLIBFILES =
###############################################################################
# #
# Path directives (-I, -R, -Q). #
# #
###############################################################################
COQMF_OCAMLLIBS = -I .
COQMF_SRC_SUBDIRS = .
COQMF_COQLIBS = -I . -R . Top
COQMF_COQLIBS_NOML = -R . Top
###############################################################################
# #
# Coq configuration. #
# #
###############################################################################
COQMF_LOCAL=0
COQMF_COQLIB=/nix/store/spk2rhfqxzrw1pyb7i6ch2kgq0mk8ja2-coq-8.7.2/lib/coq/
COQMF_DOCDIR=/nix/store/spk2rhfqxzrw1pyb7i6ch2kgq0mk8ja2-coq-8.7.2/share/doc/coq/
COQMF_OCAMLFIND=/nix/store/i8kd4i6smcbq5b4fw8q237nbkknnz3ih-ocaml-findlib-1.8.0/bin/ocamlfind
COQMF_CAMLP4=camlp5
COQMF_CAMLP4O=/nix/store/m2pz22j49byy8bk05wisqccypjq62434-camlp5-7.05/bin/camlp5o
COQMF_CAMLP4BIN=/nix/store/m2pz22j49byy8bk05wisqccypjq62434-camlp5-7.05/bin/
COQMF_CAMLP4LIB=/dev/null
COQMF_CAMLP4OPTIONS=-loc loc
COQMF_CAMLFLAGS=-thread -rectypes -w +a-4-9-27-41-42-44-45-48-50 -safe-string
COQMF_HASNATDYNLINK=true
COQMF_COQ_SRC_SUBDIRS=config dev lib kernel library engine pretyping interp parsing proofs tactics toplevel printing intf grammar ide stm vernac plugins/btauto plugins/cc plugins/derive plugins/extraction plugins/firstorder plugins/fourier plugins/funind plugins/ltac plugins/micromega plugins/nsatz plugins/omega plugins/quote plugins/romega plugins/rtauto plugins/setoid_ring plugins/ssr plugins/ssrmatching plugins/syntax plugins/xml
COQMF_WINDRIVE=/nix/store/spk2rhfqxzrw1pyb7i6ch2kgq0mk8ja2-coq-8.7.2/lib/coq
###############################################################################
# #
# Extra variables. #
# #
###############################################################################
OTHERFLAGS =
COQLIBS =
COQMF_OTHERFLAGS =
COQMF_INSTALLCOQDOCROOT = Top