-
Notifications
You must be signed in to change notification settings - Fork 5
/
Makefile.coq.conf
63 lines (52 loc) · 4.41 KB
/
Makefile.coq.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 Makefile.coq
###############################################################################
# #
# Project files. #
# #
###############################################################################
COQMF_VFILES = src/Config.v src/BabyJubjub.v src/Circom.v src/Repr.v src/ReprZ.v src/Util.v src/Default.v src/DSL.v src/CTuple.v src/Tuple.v src/ListUtil.v src/LibTactics.v src/LibOverflow.v src/PigeonHole.v src/Simplify.v src/Signed.v src/CircomLib/Comparators.v src/CircomLib/Bitify.v src/CircomLib/Gates.v src/CircomLib/Multiplexer.v src/BigInt/Definition/BigIsZero.v src/BigInt/Definition/BigIsEqual.v src/BigInt/Definition/ModProd.v src/BigInt/Definition/BigAdd.v src/BigInt/Definition/BigSub.v src/BigInt/Definition/BigLessThan.v src/BigInt/Definition/BigAddModP.v src/BigInt/Definition/BigSubModP.v src/BigInt/Definition/CheckCarryToZero.v src/BigInt/Definition/Split.v src/BigInt/Definition/BigMult.v src/BigInt/Definition/BigMod.v src/BigInt/Proof/BigIsZero.v src/BigInt/Proof/BigIsEqual.v src/BigInt/Proof/ModProd.v src/BigInt/Proof/BigAdd.v src/BigInt/Proof/BigSub.v src/BigInt/Proof/BigLessThan.v src/BigInt/Proof/BigAddModP.v src/BigInt/Proof/BigSubModP.v src/BigInt/Proof/CheckCarryToZero.v src/BigInt/Proof/Split.v src/BigInt/Theory/Polynom.v src/BigInt/Theory/Polynom_test.v src/BigInt/Proof/BigMult.v src/BigInt/Proof/BigMod.v src/BigInt/Specification.v src/CircomLib/EdDSA.v src/Sismo/hydra.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 src Circom
COQMF_COQLIBS_NOML = -R src Circom
COQMF_CMDLINE_COQLIBS =
###############################################################################
# #
# Coq configuration. #
# #
###############################################################################
COQMF_COQLIB=/home/m1stake/.opam/4.13.1/lib/coq/
COQMF_COQCORELIB=/home/m1stake/.opam/4.13.1/lib/coq/../coq-core/
COQMF_DOCDIR=/home/m1stake/.opam/4.13.1/doc/coq/
COQMF_OCAMLFIND=/home/m1stake/.opam/4.13.1/bin/ocamlfind
COQMF_CAMLFLAGS=-thread -rectypes -w -a+1..3-4+5..8-9+10..26-27+28..40-41-42+43-44-45+46..47-48+49..57-58+59..66-67-68+69-70 -safe-string -strict-sequence
COQMF_WARN=-warn-error +a-3
COQMF_HASNATDYNLINK=true
COQMF_COQ_SRC_SUBDIRS=boot 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/ltac2 plugins/micromega plugins/nsatz plugins/ring plugins/rtauto plugins/ssr plugins/ssrmatching plugins/syntax
COQMF_COQ_NATIVE_COMPILER_DEFAULT=no
COQMF_WINDRIVE=
###############################################################################
# #
# Native compiler. #
# #
###############################################################################
COQMF_COQPROJECTNATIVEFLAG =
###############################################################################
# #
# Extra variables. #
# #
###############################################################################
COQMF_OTHERFLAGS =
COQMF_INSTALLCOQDOCROOT = Circom