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
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
|
#
# General variables
#
TOPDIR=../../..
# Files with axioms to be realized: can't be extracted directly
AXIOMSVO:= \
theories/Init/Prelude.vo \
theories/Reals/% \
theories/Num/%
DIRS:= $(shell (cd $(TOPDIR);find theories -type d ! -name CVS))
INCL:= $(patsubst %,-i%,$(DIRS))
VO:= $(shell (cd $(TOPDIR);find theories -name \*.vo))
VO:= $(filter-out $(AXIOMSVO),$(VO))
HS:= $(shell test -x v2hs && ./v2hs $(VO))
O:= $(patsubst %.hs,%.o,$(HS))
#
# General rules
#
all: v2hs hs $(O)
hs: $(HS)
tree:
mkdir -p $(DIRS)
%.o:%.hs
ghc $(INCL) -c $<
$(HS): hs2v
./extract.haskell $@
clean:
rm -f theories/*/*.h* theories/*/*.o
#
# Utilities
#
hs2v: hs2v.ml
ocamlc -o $@ $<
v2hs: v2hs.ml
ocamlc -o $@ $<
$(MAKE) -f Makefile.haskell
#
# The End
#
.PHONY: all tree clean depend
# DO NOT DELETE: Beginning of Haskell dependencies
theories/Arith/Between.o : theories/Arith/Between.hs
theories/Arith/Bool_nat.o : theories/Arith/Bool_nat.hs
theories/Arith/Bool_nat.o : theories/Bool/Sumbool.o
theories/Arith/Bool_nat.o : theories/Init/Specif.o
theories/Arith/Bool_nat.o : theories/Arith/Peano_dec.o
theories/Arith/Bool_nat.o : theories/Init/Datatypes.o
theories/Arith/Bool_nat.o : theories/Arith/Compare_dec.o
theories/Arith/Compare_dec.o : theories/Arith/Compare_dec.hs
theories/Arith/Compare_dec.o : theories/Init/Specif.o
theories/Arith/Compare_dec.o : theories/Init/Logic.o
theories/Arith/Compare_dec.o : theories/Init/Datatypes.o
theories/Arith/Compare.o : theories/Arith/Compare.hs
theories/Arith/Compare.o : theories/Init/Specif.o
theories/Arith/Compare.o : theories/Init/Datatypes.o
theories/Arith/Compare.o : theories/Arith/Compare_dec.o
theories/Arith/Div2.o : theories/Arith/Div2.hs
theories/Arith/Div2.o : theories/Init/Specif.o
theories/Arith/Div2.o : theories/Init/Peano.o
theories/Arith/Div2.o : theories/Init/Datatypes.o
theories/Arith/EqNat.o : theories/Arith/EqNat.hs
theories/Arith/EqNat.o : theories/Init/Specif.o
theories/Arith/EqNat.o : theories/Init/Datatypes.o
theories/Arith/Euclid.o : theories/Arith/Euclid.hs
theories/Arith/Euclid.o : theories/Arith/Wf_nat.o
theories/Arith/Euclid.o : theories/Init/Specif.o
theories/Arith/Euclid.o : theories/Arith/Minus.o
theories/Arith/Euclid.o : theories/Init/Datatypes.o
theories/Arith/Euclid.o : theories/Arith/Compare_dec.o
theories/Arith/Even.o : theories/Arith/Even.hs
theories/Arith/Even.o : theories/Init/Specif.o
theories/Arith/Even.o : theories/Init/Datatypes.o
theories/Arith/Gt.o : theories/Arith/Gt.hs
theories/Arith/Le.o : theories/Arith/Le.hs
theories/Arith/Lt.o : theories/Arith/Lt.hs
theories/Arith/Max.o : theories/Arith/Max.hs
theories/Arith/Max.o : theories/Init/Specif.o
theories/Arith/Max.o : theories/Init/Logic.o
theories/Arith/Max.o : theories/Init/Datatypes.o
theories/Arith/Min.o : theories/Arith/Min.hs
theories/Arith/Min.o : theories/Init/Specif.o
theories/Arith/Min.o : theories/Init/Logic.o
theories/Arith/Min.o : theories/Init/Datatypes.o
theories/Arith/Minus.o : theories/Arith/Minus.hs
theories/Arith/Minus.o : theories/Init/Datatypes.o
theories/Arith/Mult.o : theories/Arith/Mult.hs
theories/Arith/Mult.o : theories/Arith/Plus.o
theories/Arith/Mult.o : theories/Init/Datatypes.o
theories/Arith/Peano_dec.o : theories/Arith/Peano_dec.hs
theories/Arith/Peano_dec.o : theories/Init/Specif.o
theories/Arith/Peano_dec.o : theories/Init/Datatypes.o
theories/Arith/Plus.o : theories/Arith/Plus.hs
theories/Arith/Plus.o : theories/Init/Specif.o
theories/Arith/Plus.o : theories/Init/Logic.o
theories/Arith/Plus.o : theories/Init/Datatypes.o
theories/Arith/Wf_nat.o : theories/Arith/Wf_nat.hs
theories/Arith/Wf_nat.o : theories/Init/Wf.o
theories/Arith/Wf_nat.o : theories/Init/Logic.o
theories/Arith/Wf_nat.o : theories/Init/Datatypes.o
theories/Bool/BoolEq.o : theories/Bool/BoolEq.hs
theories/Bool/BoolEq.o : theories/Init/Specif.o
theories/Bool/BoolEq.o : theories/Init/Datatypes.o
theories/Bool/Bool.o : theories/Bool/Bool.hs
theories/Bool/Bool.o : theories/Init/Specif.o
theories/Bool/Bool.o : theories/Init/Datatypes.o
theories/Bool/DecBool.o : theories/Bool/DecBool.hs
theories/Bool/DecBool.o : theories/Init/Specif.o
theories/Bool/IfProp.o : theories/Bool/IfProp.hs
theories/Bool/IfProp.o : theories/Init/Specif.o
theories/Bool/IfProp.o : theories/Init/Datatypes.o
theories/Bool/Sumbool.o : theories/Bool/Sumbool.hs
theories/Bool/Sumbool.o : theories/Init/Specif.o
theories/Bool/Sumbool.o : theories/Init/Datatypes.o
theories/Bool/Zerob.o : theories/Bool/Zerob.hs
theories/Bool/Zerob.o : theories/Init/Datatypes.o
theories/Init/Datatypes.o : theories/Init/Datatypes.hs
theories/Init/DatatypesSyntax.o : theories/Init/DatatypesSyntax.hs
theories/Init/Logic.o : theories/Init/Logic.hs
theories/Init/LogicSyntax.o : theories/Init/LogicSyntax.hs
theories/Init/Logic_Type.o : theories/Init/Logic_Type.hs
theories/Init/Logic_TypeSyntax.o : theories/Init/Logic_TypeSyntax.hs
theories/Init/Peano.o : theories/Init/Peano.hs
theories/Init/Peano.o : theories/Init/Datatypes.o
theories/Init/Specif.o : theories/Init/Specif.hs
theories/Init/Specif.o : theories/Init/Logic.o
theories/Init/Specif.o : theories/Init/Datatypes.o
theories/Init/SpecifSyntax.o : theories/Init/SpecifSyntax.hs
theories/Init/Wf.o : theories/Init/Wf.hs
theories/IntMap/Adalloc.o : theories/IntMap/Adalloc.hs
theories/IntMap/Adalloc.o : theories/ZArith/Fast_integer.o
theories/IntMap/Adalloc.o : theories/Bool/Sumbool.o
theories/IntMap/Adalloc.o : theories/Init/Specif.o
theories/IntMap/Adalloc.o : theories/IntMap/Map.o
theories/IntMap/Adalloc.o : theories/Init/Logic.o
theories/IntMap/Adalloc.o : theories/Init/Datatypes.o
theories/IntMap/Adalloc.o : theories/IntMap/Addr.o
theories/IntMap/Adalloc.o : theories/IntMap/Addec.o
theories/IntMap/Addec.o : theories/IntMap/Addec.hs
theories/IntMap/Addec.o : theories/ZArith/Fast_integer.o
theories/IntMap/Addec.o : theories/Bool/Sumbool.o
theories/IntMap/Addec.o : theories/Init/Specif.o
theories/IntMap/Addec.o : theories/Init/Datatypes.o
theories/IntMap/Addec.o : theories/IntMap/Addr.o
theories/IntMap/Addr.o : theories/IntMap/Addr.hs
theories/IntMap/Addr.o : theories/ZArith/Fast_integer.o
theories/IntMap/Addr.o : theories/Init/Specif.o
theories/IntMap/Addr.o : theories/Init/Datatypes.o
theories/IntMap/Addr.o : theories/Bool/Bool.o
theories/IntMap/Adist.o : theories/IntMap/Adist.hs
theories/IntMap/Adist.o : theories/ZArith/Fast_integer.o
theories/IntMap/Adist.o : theories/Arith/Min.o
theories/IntMap/Adist.o : theories/Init/Datatypes.o
theories/IntMap/Adist.o : theories/IntMap/Addr.o
theories/IntMap/Allmaps.o : theories/IntMap/Allmaps.hs
theories/IntMap/Fset.o : theories/IntMap/Fset.hs
theories/IntMap/Fset.o : theories/Init/Specif.o
theories/IntMap/Fset.o : theories/IntMap/Map.o
theories/IntMap/Fset.o : theories/Init/Logic.o
theories/IntMap/Fset.o : theories/Init/Datatypes.o
theories/IntMap/Fset.o : theories/IntMap/Addr.o
theories/IntMap/Fset.o : theories/IntMap/Addec.o
theories/IntMap/Lsort.o : theories/IntMap/Lsort.hs
theories/IntMap/Lsort.o : theories/ZArith/Fast_integer.o
theories/IntMap/Lsort.o : theories/Bool/Sumbool.o
theories/IntMap/Lsort.o : theories/Init/Specif.o
theories/IntMap/Lsort.o : theories/Lists/PolyList.o
theories/IntMap/Lsort.o : theories/IntMap/Mapiter.o
theories/IntMap/Lsort.o : theories/IntMap/Map.o
theories/IntMap/Lsort.o : theories/Init/Logic.o
theories/IntMap/Lsort.o : theories/Init/Datatypes.o
theories/IntMap/Lsort.o : theories/Bool/Bool.o
theories/IntMap/Lsort.o : theories/IntMap/Addr.o
theories/IntMap/Lsort.o : theories/IntMap/Addec.o
theories/IntMap/Mapaxioms.o : theories/IntMap/Mapaxioms.hs
theories/IntMap/Mapcanon.o : theories/IntMap/Mapcanon.hs
theories/IntMap/Mapcanon.o : theories/Init/Specif.o
theories/IntMap/Mapcanon.o : theories/IntMap/Map.o
theories/IntMap/Mapcard.o : theories/IntMap/Mapcard.hs
theories/IntMap/Mapcard.o : theories/Bool/Sumbool.o
theories/IntMap/Mapcard.o : theories/Init/Specif.o
theories/IntMap/Mapcard.o : theories/Arith/Plus.o
theories/IntMap/Mapcard.o : theories/Arith/Peano_dec.o
theories/IntMap/Mapcard.o : theories/Init/Peano.o
theories/IntMap/Mapcard.o : theories/IntMap/Map.o
theories/IntMap/Mapcard.o : theories/Init/Logic.o
theories/IntMap/Mapcard.o : theories/Init/Datatypes.o
theories/IntMap/Mapcard.o : theories/IntMap/Addr.o
theories/IntMap/Mapcard.o : theories/IntMap/Addec.o
theories/IntMap/Mapc.o : theories/IntMap/Mapc.hs
theories/IntMap/Mapfold.o : theories/IntMap/Mapfold.hs
theories/IntMap/Mapfold.o : theories/Init/Specif.o
theories/IntMap/Mapfold.o : theories/IntMap/Mapiter.o
theories/IntMap/Mapfold.o : theories/IntMap/Map.o
theories/IntMap/Mapfold.o : theories/Init/Logic.o
theories/IntMap/Mapfold.o : theories/IntMap/Fset.o
theories/IntMap/Mapfold.o : theories/Init/Datatypes.o
theories/IntMap/Mapfold.o : theories/IntMap/Addr.o
theories/IntMap/Map.o : theories/IntMap/Map.hs
theories/IntMap/Map.o : theories/ZArith/Fast_integer.o
theories/IntMap/Map.o : theories/Init/Specif.o
theories/IntMap/Map.o : theories/Init/Peano.o
theories/IntMap/Map.o : theories/Init/Datatypes.o
theories/IntMap/Map.o : theories/IntMap/Addr.o
theories/IntMap/Map.o : theories/IntMap/Addec.o
theories/IntMap/Mapiter.o : theories/IntMap/Mapiter.hs
theories/IntMap/Mapiter.o : theories/Bool/Sumbool.o
theories/IntMap/Mapiter.o : theories/Init/Specif.o
theories/IntMap/Mapiter.o : theories/Lists/PolyList.o
theories/IntMap/Mapiter.o : theories/IntMap/Map.o
theories/IntMap/Mapiter.o : theories/Init/Logic.o
theories/IntMap/Mapiter.o : theories/Init/Datatypes.o
theories/IntMap/Mapiter.o : theories/IntMap/Addr.o
theories/IntMap/Mapiter.o : theories/IntMap/Addec.o
theories/IntMap/Maplists.o : theories/IntMap/Maplists.hs
theories/IntMap/Maplists.o : theories/Bool/Sumbool.o
theories/IntMap/Maplists.o : theories/Init/Specif.o
theories/IntMap/Maplists.o : theories/Lists/PolyList.o
theories/IntMap/Maplists.o : theories/IntMap/Mapiter.o
theories/IntMap/Maplists.o : theories/IntMap/Map.o
theories/IntMap/Maplists.o : theories/Init/Logic.o
theories/IntMap/Maplists.o : theories/IntMap/Fset.o
theories/IntMap/Maplists.o : theories/Init/Datatypes.o
theories/IntMap/Maplists.o : theories/Bool/Bool.o
theories/IntMap/Maplists.o : theories/IntMap/Addr.o
theories/IntMap/Maplists.o : theories/IntMap/Addec.o
theories/IntMap/Mapsubset.o : theories/IntMap/Mapsubset.hs
theories/IntMap/Mapsubset.o : theories/IntMap/Mapiter.o
theories/IntMap/Mapsubset.o : theories/IntMap/Map.o
theories/IntMap/Mapsubset.o : theories/IntMap/Fset.o
theories/IntMap/Mapsubset.o : theories/Init/Datatypes.o
theories/IntMap/Mapsubset.o : theories/Bool/Bool.o
theories/Lists/ListSet.o : theories/Lists/ListSet.hs
theories/Lists/ListSet.o : theories/Init/Specif.o
theories/Lists/ListSet.o : theories/Lists/PolyList.o
theories/Lists/ListSet.o : theories/Init/Logic.o
theories/Lists/ListSet.o : theories/Init/Datatypes.o
theories/Lists/PolyList.o : theories/Lists/PolyList.hs
theories/Lists/PolyList.o : theories/Init/Specif.o
theories/Lists/PolyList.o : theories/Init/Datatypes.o
theories/Lists/PolyListSyntax.o : theories/Lists/PolyListSyntax.hs
theories/Lists/Streams.o : theories/Lists/Streams.hs
theories/Lists/Streams.o : theories/Init/Datatypes.o
theories/Lists/TheoryList.o : theories/Lists/TheoryList.hs
theories/Lists/TheoryList.o : theories/Init/Specif.o
theories/Lists/TheoryList.o : theories/Lists/PolyList.o
theories/Lists/TheoryList.o : theories/Bool/DecBool.o
theories/Lists/TheoryList.o : theories/Init/Datatypes.o
theories/Logic/Berardi.o : theories/Logic/Berardi.hs
theories/Logic/ClassicalFacts.o : theories/Logic/ClassicalFacts.hs
theories/Logic/Classical.o : theories/Logic/Classical.hs
theories/Logic/Classical_Pred_Set.o : theories/Logic/Classical_Pred_Set.hs
theories/Logic/Classical_Pred_Type.o : theories/Logic/Classical_Pred_Type.hs
theories/Logic/Classical_Prop.o : theories/Logic/Classical_Prop.hs
theories/Logic/Classical_Type.o : theories/Logic/Classical_Type.hs
theories/Logic/Decidable.o : theories/Logic/Decidable.hs
theories/Logic/Eqdep_dec.o : theories/Logic/Eqdep_dec.hs
theories/Logic/Eqdep.o : theories/Logic/Eqdep.hs
theories/Logic/Hurkens.o : theories/Logic/Hurkens.hs
theories/Logic/JMeq.o : theories/Logic/JMeq.hs
theories/Logic/ProofIrrelevance.o : theories/Logic/ProofIrrelevance.hs
theories/Relations/Newman.o : theories/Relations/Newman.hs
theories/Relations/Operators_Properties.o : theories/Relations/Operators_Properties.hs
theories/Relations/Relation_Definitions.o : theories/Relations/Relation_Definitions.hs
theories/Relations/Relation_Operators.o : theories/Relations/Relation_Operators.hs
theories/Relations/Relation_Operators.o : theories/Init/Specif.o
theories/Relations/Relation_Operators.o : theories/Lists/PolyList.o
theories/Relations/Relations.o : theories/Relations/Relations.hs
theories/Relations/Rstar.o : theories/Relations/Rstar.hs
theories/Setoids/Setoid.o : theories/Setoids/Setoid.hs
theories/Sets/Classical_sets.o : theories/Sets/Classical_sets.hs
theories/Sets/Constructive_sets.o : theories/Sets/Constructive_sets.hs
theories/Sets/Cpo.o : theories/Sets/Cpo.hs
theories/Sets/Cpo.o : theories/Sets/Partial_Order.o
theories/Sets/Ensembles.o : theories/Sets/Ensembles.hs
theories/Sets/Finite_sets_facts.o : theories/Sets/Finite_sets_facts.hs
theories/Sets/Finite_sets.o : theories/Sets/Finite_sets.hs
theories/Sets/Image.o : theories/Sets/Image.hs
theories/Sets/Infinite_sets.o : theories/Sets/Infinite_sets.hs
theories/Sets/Integers.o : theories/Sets/Integers.hs
theories/Sets/Integers.o : theories/Sets/Partial_Order.o
theories/Sets/Integers.o : theories/Init/Datatypes.o
theories/Sets/Multiset.o : theories/Sets/Multiset.hs
theories/Sets/Multiset.o : theories/Init/Specif.o
theories/Sets/Multiset.o : theories/Init/Peano.o
theories/Sets/Multiset.o : theories/Init/Datatypes.o
theories/Sets/Partial_Order.o : theories/Sets/Partial_Order.hs
theories/Sets/Permut.o : theories/Sets/Permut.hs
theories/Sets/Powerset_Classical_facts.o : theories/Sets/Powerset_Classical_facts.hs
theories/Sets/Powerset_facts.o : theories/Sets/Powerset_facts.hs
theories/Sets/Powerset.o : theories/Sets/Powerset.hs
theories/Sets/Powerset.o : theories/Sets/Partial_Order.o
theories/Sets/Relations_1_facts.o : theories/Sets/Relations_1_facts.hs
theories/Sets/Relations_1.o : theories/Sets/Relations_1.hs
theories/Sets/Relations_2_facts.o : theories/Sets/Relations_2_facts.hs
theories/Sets/Relations_2.o : theories/Sets/Relations_2.hs
theories/Sets/Relations_3_facts.o : theories/Sets/Relations_3_facts.hs
theories/Sets/Relations_3.o : theories/Sets/Relations_3.hs
theories/Sets/Uniset.o : theories/Sets/Uniset.hs
theories/Sets/Uniset.o : theories/Init/Specif.o
theories/Sets/Uniset.o : theories/Init/Datatypes.o
theories/Sets/Uniset.o : theories/Bool/Bool.o
theories/Sorting/Heap.o : theories/Sorting/Heap.hs
theories/Sorting/Heap.o : theories/Init/Specif.o
theories/Sorting/Heap.o : theories/Sorting/Sorting.o
theories/Sorting/Heap.o : theories/Lists/PolyList.o
theories/Sorting/Heap.o : theories/Sets/Multiset.o
theories/Sorting/Heap.o : theories/Init/Logic.o
theories/Sorting/Permutation.o : theories/Sorting/Permutation.hs
theories/Sorting/Permutation.o : theories/Init/Specif.o
theories/Sorting/Permutation.o : theories/Lists/PolyList.o
theories/Sorting/Permutation.o : theories/Sets/Multiset.o
theories/Sorting/Sorting.o : theories/Sorting/Sorting.hs
theories/Sorting/Sorting.o : theories/Init/Specif.o
theories/Sorting/Sorting.o : theories/Lists/PolyList.o
theories/Sorting/Sorting.o : theories/Init/Logic.o
theories/Wellfounded/Disjoint_Union.o : theories/Wellfounded/Disjoint_Union.hs
theories/Wellfounded/Inclusion.o : theories/Wellfounded/Inclusion.hs
theories/Wellfounded/Inverse_Image.o : theories/Wellfounded/Inverse_Image.hs
theories/Wellfounded/Lexicographic_Exponentiation.o : theories/Wellfounded/Lexicographic_Exponentiation.hs
theories/Wellfounded/Lexicographic_Product.o : theories/Wellfounded/Lexicographic_Product.hs
theories/Wellfounded/Transitive_Closure.o : theories/Wellfounded/Transitive_Closure.hs
theories/Wellfounded/Union.o : theories/Wellfounded/Union.hs
theories/Wellfounded/Wellfounded.o : theories/Wellfounded/Wellfounded.hs
theories/Wellfounded/Well_Ordering.o : theories/Wellfounded/Well_Ordering.hs
theories/Wellfounded/Well_Ordering.o : theories/Init/Wf.o
theories/Wellfounded/Well_Ordering.o : theories/Init/Specif.o
theories/ZArith/Auxiliary.o : theories/ZArith/Auxiliary.hs
theories/ZArith/Fast_integer.o : theories/ZArith/Fast_integer.hs
theories/ZArith/Fast_integer.o : theories/Init/Peano.o
theories/ZArith/Fast_integer.o : theories/Init/Datatypes.o
theories/ZArith/Wf_Z.o : theories/ZArith/Wf_Z.hs
theories/ZArith/Wf_Z.o : theories/ZArith/Zarith_aux.o
theories/ZArith/Wf_Z.o : theories/ZArith/Fast_integer.o
theories/ZArith/Wf_Z.o : theories/Init/Specif.o
theories/ZArith/Wf_Z.o : theories/Init/Peano.o
theories/ZArith/Wf_Z.o : theories/Init/Logic.o
theories/ZArith/Wf_Z.o : theories/Init/Datatypes.o
theories/ZArith/Zarith_aux.o : theories/ZArith/Zarith_aux.hs
theories/ZArith/Zarith_aux.o : theories/ZArith/Fast_integer.o
theories/ZArith/Zarith_aux.o : theories/Init/Specif.o
theories/ZArith/Zarith_aux.o : theories/Init/Datatypes.o
theories/ZArith/ZArith_base.o : theories/ZArith/ZArith_base.hs
theories/ZArith/ZArith_dec.o : theories/ZArith/ZArith_dec.hs
theories/ZArith/ZArith_dec.o : theories/ZArith/Fast_integer.o
theories/ZArith/ZArith_dec.o : theories/Bool/Sumbool.o
theories/ZArith/ZArith_dec.o : theories/Init/Specif.o
theories/ZArith/ZArith_dec.o : theories/Init/Logic.o
theories/ZArith/ZArith.o : theories/ZArith/ZArith.hs
theories/ZArith/Zbool.o : theories/ZArith/Zbool.hs
theories/ZArith/Zbool.o : theories/ZArith/Fast_integer.o
theories/ZArith/Zbool.o : theories/ZArith/Zmisc.o
theories/ZArith/Zbool.o : theories/ZArith/ZArith_dec.o
theories/ZArith/Zbool.o : theories/Bool/Sumbool.o
theories/ZArith/Zbool.o : theories/Init/Specif.o
theories/ZArith/Zbool.o : theories/Init/Datatypes.o
theories/ZArith/Zcomplements.o : theories/ZArith/Zcomplements.hs
theories/ZArith/Zcomplements.o : theories/ZArith/Zarith_aux.o
theories/ZArith/Zcomplements.o : theories/ZArith/Fast_integer.o
theories/ZArith/Zcomplements.o : theories/ZArith/Wf_Z.o
theories/ZArith/Zcomplements.o : theories/Init/Specif.o
theories/ZArith/Zcomplements.o : theories/Init/Logic.o
theories/ZArith/Zcomplements.o : theories/Init/Datatypes.o
theories/ZArith/Zdiv.o : theories/ZArith/Zdiv.hs
theories/ZArith/Zdiv.o : theories/ZArith/Zarith_aux.o
theories/ZArith/Zdiv.o : theories/ZArith/Fast_integer.o
theories/ZArith/Zdiv.o : theories/ZArith/Zmisc.o
theories/ZArith/Zdiv.o : theories/ZArith/ZArith_dec.o
theories/ZArith/Zdiv.o : theories/Init/Specif.o
theories/ZArith/Zdiv.o : theories/Init/Logic.o
theories/ZArith/Zdiv.o : theories/Init/Datatypes.o
theories/ZArith/Zhints.o : theories/ZArith/Zhints.hs
theories/ZArith/Zlogarithm.o : theories/ZArith/Zlogarithm.hs
theories/ZArith/Zlogarithm.o : theories/ZArith/Zarith_aux.o
theories/ZArith/Zlogarithm.o : theories/ZArith/Fast_integer.o
theories/ZArith/Zmisc.o : theories/ZArith/Zmisc.hs
theories/ZArith/Zmisc.o : theories/ZArith/Fast_integer.o
theories/ZArith/Zmisc.o : theories/Init/Specif.o
theories/ZArith/Zmisc.o : theories/Init/Datatypes.o
theories/ZArith/Zpower.o : theories/ZArith/Zpower.hs
theories/ZArith/Zpower.o : theories/ZArith/Zarith_aux.o
theories/ZArith/Zpower.o : theories/ZArith/Fast_integer.o
theories/ZArith/Zpower.o : theories/ZArith/Zmisc.o
theories/ZArith/Zpower.o : theories/Init/Logic.o
theories/ZArith/Zpower.o : theories/Init/Datatypes.o
theories/ZArith/Zsqrt.o : theories/ZArith/Zsqrt.hs
theories/ZArith/Zsqrt.o : theories/ZArith/Zarith_aux.o
theories/ZArith/Zsqrt.o : theories/ZArith/Fast_integer.o
theories/ZArith/Zsqrt.o : theories/ZArith/ZArith_dec.o
theories/ZArith/Zsqrt.o : theories/Init/Specif.o
theories/ZArith/Zsqrt.o : theories/Init/Logic.o
theories/ZArith/Zwf.o : theories/ZArith/Zwf.hs
# DO NOT DELETE: End of Haskell dependencies
|
