blob: 7c4497e2ea2017be1ec4454ebc9ceda80a508891 (
plain)
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
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
|
########################################################################
## This file is intended to developers, please do not use it to ##
## generate a Makefile, rather use the provided Makefile. ##
########################################################################
########################################################################
## To generate the Makefile: ##
## coq_makefile -f Make -o Makefile ##
## Suppress the "Makefile" target ##
## Change the "all" target into: ##
## all: ml $(CMXFILES) $(CMXA) $(CMXS) $(VOFILES) ##
## Change the "install-natdynlink" target: change CMXSFILES into CMXS and add the same thing for CMXA. ##
## Change the "install" target: change CMO into CMX. ##
## Remove the automatically generated line with %.cmxs: %.cmx ##
## Finally, suppress the "Makefile" target and add to the "clean" target: ##
## - rm -f ../unit-tests/*.vo ../unit-tests/*.zlog ../unit-tests/*.vtlog verit/veritParser.mli verit/veritParser.ml verit/veritLexer.ml smtlib2/smtlib2_parse.mli smtlib2/smtlib2_parse.ml smtlib2/smtlib2_lex.ml smtcoq.a ##
########################################################################
-R . SMTCoq
-I .
-I cnf
-I euf
-I lia
-I smtlib2
-I trace
-I verit
-I zchaff
-I versions/standard
-I versions/standard/Int63
-I versions/standard/Array
-I $(COQBIN)../plugins/micromega
# -extra "test" "" "cd ../unit-tests; make" ""
# -extra "ztest" "" "cd ../unit-tests; make zchaff"
# -extra "vtest" "" "cd ../unit-tests; make verit"
-extra "%.ml" "%.mll" "$(CAMLLEX) $<"
-extra "%.ml %.mli" "%.mly" "$(CAMLYACC) $<"
-extra-phony "smtcoq_plugin.mlpack.d" "verit/veritParser.ml verit/veritLexer.ml smtlib2/smtlib2_parse.ml smtlib2/smtlib2_lex.ml" ""
CAMLLEX = $(CAMLBIN)ocamllex
CAMLYACC = $(CAMLBIN)ocamlyacc
versions/standard/Int63/Int63.v
versions/standard/Int63/Int63Native.v
versions/standard/Int63/Int63Op.v
versions/standard/Int63/Int63Axioms.v
versions/standard/Int63/Int63Properties.v
versions/standard/Array/PArray.v
versions/standard/Structures.v
versions/standard/structures.ml
trace/coqTerms.ml
trace/satAtom.ml
trace/smtAtom.ml
trace/smtAtom.mli
trace/smtCertif.ml
trace/smtCnf.ml
trace/smtCommands.ml
trace/smtForm.ml
trace/smtForm.mli
trace/smtMisc.ml
trace/smtTrace.ml
smtlib2/smtlib2_parse.ml
smtlib2/smtlib2_parse.mli
smtlib2/smtlib2_ast.ml
smtlib2/smtlib2_genConstr.ml
smtlib2/smtlib2_lex.ml
smtlib2/smtlib2_util.ml
verit/veritParser.ml
verit/veritParser.mli
verit/verit.ml
verit/veritLexer.ml
verit/veritSyntax.ml
verit/veritSyntax.mli
zchaff/cnfParser.ml
zchaff/satParser.ml
zchaff/zchaff.ml
zchaff/zchaffParser.ml
cnf/Cnf.v
euf/Euf.v
lia/lia.ml
lia/Lia.v
spl/Assumptions.v
spl/Syntactic.v
spl/Arithmetic.v
spl/Operators.v
Misc.v
SMTCoq.v
SMT_terms.v
State.v
Trace.v
g_smtcoq.ml4
smtcoq_plugin.mlpack
|
