Ticket #48155: main.log

File main.log, 83.4 KB (added by lord@…, 9 years ago)
Line 
1version:1
2:debug:main epoch: in tree: 1 installed: 1
3:debug:main ocaml 4.02.2_0 exists in the ports tree
4:debug:main ocaml 4.02.2_0  is the latest installed
5:debug:main ocaml 4.02.2_0  is active
6:debug:main Merging existing variants '' into variants
7:debug:main new fully merged portvariants:
8:debug:main Changing to port directory: /opt/local/var/macports/sources/rsync.macports.org/release/tarballs/ports/lang/ocaml
9:debug:main OS darwin/14.3.0 (Mac OS X 10.10) arch i386
10:debug:main universal_variant is false, so not adding the default universal variant
11:debug:main Running callback portconfigure::add_automatic_compiler_dependencies
12:debug:main Finished running callback portconfigure::add_automatic_compiler_dependencies
13:debug:main Running callback portbuild::add_automatic_buildsystem_dependencies
14:debug:main Finished running callback portbuild::add_automatic_buildsystem_dependencies
15:debug:main No need to upgrade! ocaml 4.02.2_0 >= ocaml 4.02.2_0
16:debug:main epoch: in tree: 0 installed: 0
17:debug:main ncurses 5.9_2 exists in the ports tree
18:debug:main ncurses 5.9_2 +universal is the latest installed
19:debug:main ncurses 5.9_2 +universal is active
20:debug:main Merging existing variants '+universal' into variants
21:debug:main new fully merged portvariants: universal +
22:debug:main Changing to port directory: /opt/local/var/macports/sources/rsync.macports.org/release/tarballs/ports/devel/ncurses
23:debug:main OS darwin/14.3.0 (Mac OS X 10.10) arch i386
24:debug:main adding the default universal variant
25:debug:main Reading variant descriptions from /opt/local/var/macports/sources/rsync.macports.org/release/tarballs/ports/_resources/port1.0/variant_descriptions.conf
26:debug:main Executing variant universal provides universal
27:debug:main Running callback portconfigure::add_automatic_compiler_dependencies
28:debug:main Finished running callback portconfigure::add_automatic_compiler_dependencies
29:debug:main Running callback portbuild::add_automatic_buildsystem_dependencies
30:debug:main Finished running callback portbuild::add_automatic_buildsystem_dependencies
31:debug:main No need to upgrade! ncurses 5.9_2 >= ncurses 5.9_2
32:debug:main epoch: in tree: 0 installed: 0
33:debug:main camlp5 6.12_0 exists in the ports tree
34:debug:main camlp5 6.12_0  is the latest installed
35:debug:main camlp5 6.12_0  is active
36:debug:main Merging existing variants '' into variants
37:debug:main new fully merged portvariants:
38:debug:main Changing to port directory: /opt/local/var/macports/sources/rsync.macports.org/release/tarballs/ports/lang/camlp5
39:debug:main OS darwin/14.3.0 (Mac OS X 10.10) arch i386
40:debug:main universal_variant is false, so not adding the default universal variant
41:debug:main Running callback portconfigure::add_automatic_compiler_dependencies
42:debug:main Finished running callback portconfigure::add_automatic_compiler_dependencies
43:debug:main Running callback portbuild::add_automatic_buildsystem_dependencies
44:debug:main Finished running callback portbuild::add_automatic_buildsystem_dependencies
45:debug:main No need to upgrade! camlp5 6.12_0 >= camlp5 6.12_0
46:msg:main --->  Computing dependencies for coq:info:main .:debug:main coq has no conflicts
47:debug:main Searching for dependency: ocaml
48:debug:main Found Dependency: receipt exists for ocaml
49:debug:main Searching for dependency: camlp5
50:debug:main Found Dependency: receipt exists for camlp5
51:msg:main
52:debug:main Executing org.macports.main (coq)
53:debug:main changing euid/egid - current euid: 0 - current egid: 0
54:debug:main egid changed to: 20
55:debug:main euid changed to: 502
56:debug:archivefetch archivefetch phase started at Tue Jun 23 18:16:30 PDT 2015
57:msg:archivefetch --->  Fetching archive for coq
58:debug:archivefetch Executing org.macports.archivefetch (coq)
59:debug:archivefetch euid/egid changed to: 0/0
60:debug:archivefetch chowned /opt/local/var/macports/incoming to macports
61:debug:archivefetch euid/egid changed to: 502/20
62:info:archivefetch --->  coq-8.4pl6_0.darwin_14.x86_64.tbz2 doesn't seem to exist in /opt/local/var/macports/incoming/verified
63:msg:archivefetch --->  Attempting to fetch coq-8.4pl6_0.darwin_14.x86_64.tbz2 from http://packages.macports.org/coq
64:debug:archivefetch Fetching archive failed:: The requested URL returned error: 404 Not Found
65:msg:archivefetch --->  Attempting to fetch coq-8.4pl6_0.darwin_14.x86_64.tbz2 from http://lil.fr.packages.macports.org/coq
66:debug:archivefetch Fetching archive failed:: The requested URL returned error: 404 Not Found
67:msg:archivefetch --->  Attempting to fetch coq-8.4pl6_0.darwin_14.x86_64.tbz2 from http://mse.uk.packages.macports.org/sites/packages.macports.org/coq
68:debug:archivefetch Fetching archive failed:: The requested URL returned error: 404 Not Found
69:debug:archivefetch Privilege de-escalation not attempted as not running as root.
70:debug:fetch fetch phase started at Tue Jun 23 18:16:31 PDT 2015
71:notice:fetch --->  Fetching distfiles for coq
72:debug:fetch Executing org.macports.fetch (coq)
73:debug:fetch Privilege de-escalation not attempted as not running as root.
74:debug:checksum checksum phase started at Tue Jun 23 18:16:31 PDT 2015
75:notice:checksum --->  Verifying checksums for coq
76:debug:checksum Executing org.macports.checksum (coq)
77:info:checksum --->  Checksumming coq-8.4pl6.tar.gz
78:debug:checksum Calculated (rmd160) is f57f6e5732d3977f3346dda2749f4b9628604018
79:debug:checksum Correct (rmd160) checksum for coq-8.4pl6.tar.gz
80:debug:checksum Calculated (sha256) is a540a231a9970a49353ca039f3544616ff86a208966ab1c593779ae13c91ebd6
81:debug:checksum Correct (sha256) checksum for coq-8.4pl6.tar.gz
82:debug:checksum Privilege de-escalation not attempted as not running as root.
83:debug:extract extract phase started at Tue Jun 23 18:16:31 PDT 2015
84:notice:extract --->  Extracting coq
85:debug:extract Executing org.macports.extract (coq)
86:info:extract --->  Extracting coq-8.4pl6.tar.gz
87:debug:extract setting option extract.args to '/opt/local/var/macports/distfiles/coq/coq-8.4pl6.tar.gz'
88:debug:extract Environment:
89CC_PRINT_OPTIONS='YES'
90CC_PRINT_OPTIONS_FILE='/opt/local/var/macports/build/_opt_local_var_macports_sources_rsync.macports.org_release_tarballs_ports_lang_coq/coq/work/.CC_PRINT_OPTIONS'
91CPATH='/opt/local/include'
92LIBRARY_PATH='/opt/local/lib'
93MACOSX_DEPLOYMENT_TARGET='10.10'
94:debug:extract Assembled command: 'cd "/opt/local/var/macports/build/_opt_local_var_macports_sources_rsync.macports.org_release_tarballs_ports_lang_coq/coq/work" && /usr/bin/gzip -dc '/opt/local/var/macports/distfiles/coq/coq-8.4pl6.tar.gz' | /usr/bin/tar -xf -'
95:debug:extract Executing command line:  cd "/opt/local/var/macports/build/_opt_local_var_macports_sources_rsync.macports.org_release_tarballs_ports_lang_coq/coq/work" && /usr/bin/gzip -dc '/opt/local/var/macports/distfiles/coq/coq-8.4pl6.tar.gz' | /usr/bin/tar -xf -
96:debug:extract euid/egid changed to: 0/0
97:debug:extract chowned /opt/local/var/macports/build/_opt_local_var_macports_sources_rsync.macports.org_release_tarballs_ports_lang_coq/coq/work to macports
98:debug:extract euid/egid changed to: 502/20
99:debug:extract Privilege de-escalation not attempted as not running as root.
100:debug:patch patch phase started at Tue Jun 23 18:16:32 PDT 2015
101:debug:patch Executing org.macports.patch (coq)
102:debug:patch Privilege de-escalation not attempted as not running as root.
103:debug:configure configure phase started at Tue Jun 23 18:16:32 PDT 2015
104:notice:configure --->  Configuring coq
105:debug:configure Using compiler 'Xcode Clang'
106:debug:configure Executing org.macports.configure (coq)
107:debug:configure Environment:
108CC='/usr/bin/clang'
109CC_PRINT_OPTIONS='YES'
110CC_PRINT_OPTIONS_FILE='/opt/local/var/macports/build/_opt_local_var_macports_sources_rsync.macports.org_release_tarballs_ports_lang_coq/coq/work/.CC_PRINT_OPTIONS'
111CFLAGS='-pipe -Os -arch x86_64'
112CPATH='/opt/local/include'
113CPPFLAGS='-I/opt/local/include'
114CXX='/usr/bin/clang++'
115CXXFLAGS='-pipe -Os -arch x86_64 -stdlib=libc++'
116F77FLAGS='-m64'
117F90FLAGS='-pipe -Os -m64'
118FCFLAGS='-pipe -Os -m64'
119FFLAGS='-pipe -Os'
120INSTALL='/usr/bin/install -c'
121LDFLAGS='-L/opt/local/lib -Wl,-headerpad_max_install_names -arch x86_64'
122LIBRARY_PATH='/opt/local/lib'
123MACOSX_DEPLOYMENT_TARGET='10.10'
124OBJC='/usr/bin/clang'
125OBJCFLAGS='-pipe -Os -arch x86_64'
126OBJCXX='/usr/bin/clang++'
127OBJCXXFLAGS='-pipe -Os -arch x86_64 -stdlib=libc++'
128:debug:configure Assembled command: 'cd "/opt/local/var/macports/build/_opt_local_var_macports_sources_rsync.macports.org_release_tarballs_ports_lang_coq/coq/work/coq-8.4pl6" && ./configure -prefix /opt/local -emacslib /opt/local/share/emacs/site-lisp/ -mandir /opt/local/share/man -coqdocdir /opt/local/share/coq/latex -coqide none -with-doc no'
129:debug:configure Executing command line:  cd "/opt/local/var/macports/build/_opt_local_var_macports_sources_rsync.macports.org_release_tarballs_ports_lang_coq/coq/work/coq-8.4pl6" && ./configure -prefix /opt/local -emacslib /opt/local/share/emacs/site-lisp/ -mandir /opt/local/share/man -coqdocdir /opt/local/share/coq/latex -coqide none -with-doc no
130:info:configure You have GNU Make 3.81. Good!
131:info:configure You have Objective-Caml 4.02.2. Good!
132:info:configure You have native-code compilation. Good!
133:info:configure CoqIde disabled as requested.
134:info:configure
135:info:configure   Coq top directory                 : /opt/local/var/macports/build/_opt_local_var_macports_sources_rsync.macports.org_release_tarballs_ports_lang_coq/coq/work/coq-8.4pl6
136:info:configure   Architecture                      : Darwin
137:info:configure   Coq VM bytecode link flags        : -custom
138:info:configure   Coq tools bytecode link flags     : -custom
139:info:configure   OS dependent libraries            : -cclib -lunix
140:info:configure   Objective-Caml/Camlp4 version     : 4.02.2
141:info:configure   Objective-Caml/Camlp4 binaries in : /opt/local/bin
142:info:configure   Objective-Caml library in         : /opt/local/lib/ocaml
143:info:configure   Camlp4 library in                 : /opt/local/lib/ocaml/camlp5
144:info:configure   Native dynamic link support       : true
145:info:configure   Documentation                     : None
146:info:configure   CoqIde                            : no
147:info:configure   Web browser                       : open %s
148:info:configure   Coq web site                      : http://coq.inria.fr/
149:info:configure
150:info:configure   Paths for true installation:
151:info:configure     binaries      will be copied in /opt/local/bin
152:info:configure     library       will be copied in /opt/local/lib/coq
153:info:configure     config files  will be copied in /opt/local/etc/xdg/coq
154:info:configure     data files    will be copied in /opt/local/share/coq
155:info:configure     man pages     will be copied in /opt/local/share/man
156:info:configure     documentation will be copied in /opt/local/share/doc/coq
157:info:configure     emacs mode    will be copied in /opt/local/share/emacs/site-lisp/
158:info:configure
159:info:configure If anything in the above is wrong, please restart './configure'.
160:info:configure
161:info:configure *Warning* To compile the system for a new architecture
162:info:configure           don't forget to do a 'make archclean' before './configure'.
163:debug:configure Privilege de-escalation not attempted as not running as root.
164:debug:build build phase started at Tue Jun 23 18:16:33 PDT 2015
165:notice:build --->  Building coq
166:debug:build Executing org.macports.build (coq)
167:debug:build Environment:
168CC_PRINT_OPTIONS='YES'
169CC_PRINT_OPTIONS_FILE='/opt/local/var/macports/build/_opt_local_var_macports_sources_rsync.macports.org_release_tarballs_ports_lang_coq/coq/work/.CC_PRINT_OPTIONS'
170CPATH='/opt/local/include'
171LIBRARY_PATH='/opt/local/lib'
172MACOSX_DEPLOYMENT_TARGET='10.10'
173:debug:build Assembled command: 'cd "/opt/local/var/macports/build/_opt_local_var_macports_sources_rsync.macports.org_release_tarballs_ports_lang_coq/coq/work/coq-8.4pl6" && /usr/bin/make -j4 -w world'
174:debug:build Executing command line:  cd "/opt/local/var/macports/build/_opt_local_var_macports_sources_rsync.macports.org_release_tarballs_ports_lang_coq/coq/work/coq-8.4pl6" && /usr/bin/make -j4 -w world
175:info:build make: Entering directory `/opt/local/var/macports/build/_opt_local_var_macports_sources_rsync.macports.org_release_tarballs_ports_lang_coq/coq/work/coq-8.4pl6'
176:info:build /Applications/Xcode.app/Contents/Developer/usr/bin/make --warn-undefined-variable --no-builtin-rules -f Makefile.build "world"
177:info:build make[1]: Entering directory `/opt/local/var/macports/build/_opt_local_var_macports_sources_rsync.macports.org_release_tarballs_ports_lang_coq/coq/work/coq-8.4pl6'
178:info:build "ocaml" theories/Numbers/Natural/BigN/NMake_gen.ml > "theories/Numbers/Natural/BigN/NMake_gen.v" || (RV=$?; rm -f "theories/Numbers/Natural/BigN/NMake_gen.v"; exit ${RV})
179:info:build OCAMLLEX  tools/coqdep_lexer.mll
180:info:build OCAMLLEX  ide/config_lexer.mll
181:info:build OCAMLLEX  ide/coq_lex.mll
182:info:build ocamllex warning:
183:info:build File "ide/coq_lex.mll", line 112, character 66: unescaped newline in string.
184:info:build 30 states, 1657 transitions, table size 6808 bytes
185:info:build 6096 additional bytes used for bindings
186:info:build OCAMLLEX  ide/utf8_convert.mll
187:info:build 15 states, 827 transitions, table size 3398 bytes
188:info:build OCAMLLEX  lib/xml_lexer.mll
189:info:build 78 states, 800 transitions, table size 3668 bytes
190:info:build OCAMLLEX  tools/coqdoc/cpretty.mll
191:info:build 348 states, 7127 transitions, table size 30596 bytes
192:info:build 3131 additional bytes used for bindings
193:info:build OCAMLLEX  tools/coqwc.mll
194:info:build OCAMLLEX  tools/gallina_lexer.mll
195:info:build 230 states, 833 transitions, table size 4712 bytes
196:info:build 190 states, 498 transitions, table size 3132 bytes
197:info:build ECHO... > scripts/tolink.ml
198:info:build sed -n -e '/^enum/p' -e 's/,//g' -e '/^  /p' kernel/byterun/coq_instruct.h | \
199:info:build     awk -f kernel/make-opcodes > "kernel/copcodes.ml" || (RV=$?; rm -f "kernel/copcodes.ml"; exit ${RV})
200:info:build sed -n -e '/^  /s/ \([A-Z]\)/ \&\&coq_lbl_\1/gp' \
201:info:build                -e '/^}/q' kernel/byterun/coq_instruct.h > "kernel/byterun/coq_jumptbl.h" || (RV=$?; rm -f "kernel/byterun/coq_jumptbl.h"; exit ${RV})
202:info:build ECHO... > plugins/cc/cc_plugin_mod.ml
203:info:build ECHO... > plugins/decl_mode/decl_mode_plugin_mod.ml
204:info:build ECHO... > plugins/extraction/extraction_plugin_mod.ml
205:info:build ECHO... > plugins/field/field_plugin_mod.ml
206:info:build ECHO... > plugins/firstorder/ground_plugin_mod.ml
207:info:build ECHO... > plugins/fourier/fourier_plugin_mod.ml
208:info:build ECHO... > plugins/funind/recdef_plugin_mod.ml
209:info:build ECHO... > plugins/micromega/micromega_plugin_mod.ml
210:info:build ECHO... > plugins/nsatz/nsatz_plugin_mod.ml
211:info:build ECHO... > plugins/omega/omega_plugin_mod.ml
212:info:build ECHO... > plugins/quote/quote_plugin_mod.ml
213:info:build ECHO... > plugins/ring/ring_plugin_mod.ml
214:info:build ECHO... > plugins/romega/romega_plugin_mod.ml
215:info:build ECHO... > plugins/rtauto/rtauto_plugin_mod.ml
216:info:build ECHO... > plugins/setoid_ring/newring_plugin_mod.ml
217:info:build ECHO... > plugins/subtac/subtac_plugin_mod.ml
218:info:build ECHO... > plugins/syntax/ascii_syntax_plugin_mod.ml
219:info:build ECHO... > plugins/syntax/nat_syntax_plugin_mod.ml
220:info:build ECHO... > plugins/syntax/numbers_syntax_plugin_mod.ml
221:info:build ECHO... > plugins/syntax/r_syntax_plugin_mod.ml
222:info:build ECHO... > plugins/syntax/string_syntax_plugin_mod.ml
223:info:build ECHO... > plugins/syntax/z_syntax_plugin_mod.ml
224:info:build ECHO... > plugins/xml/xml_plugin_mod.ml
225:info:build CCDEP     kernel/byterun/coq_values.c
226:info:build CCDEP     kernel/byterun/coq_memory.c
227:info:build CCDEP     kernel/byterun/coq_interp.c
228:info:build CCDEP     kernel/byterun/coq_fix_code.c
229:info:build CCDEP       ide/ide_win32_stubs.c
230:info:build "ocamlc" -rectypes  -c tools/compat5.ml
231:info:build "ocamlc" -rectypes  -c tools/compat5b.ml
232:info:build CAMLP4DEPS toplevel/whelp.ml4
233:info:build CAMLP4O   toplevel/mltop.ml4
234:info:build CAMLP4DEPS tactics/tauto.ml4
235:info:build CAMLP4DEPS tactics/rewrite.ml4
236:info:build CAMLP4DEPS tactics/hipattern.ml4
237:info:build CAMLP4DEPS tactics/extratactics.ml4
238:info:build CAMLP4DEPS tactics/extraargs.ml4
239:info:build CAMLP4DEPS tactics/eqdecide.ml4
240:info:build CAMLP4DEPS tactics/eauto.ml4
241:info:build CAMLP4DEPS tactics/class_tactics.ml4
242:info:build CAMLP4DEPS plugins/xml/xmlentries.ml4
243:info:build CAMLP4DEPS plugins/xml/xml.ml4
244:info:build CAMLP4DEPS plugins/xml/proofTree2Xml.ml4
245:info:build CAMLP4DEPS plugins/xml/dumptree.ml4
246:info:build CAMLP4DEPS plugins/xml/acic2Xml.ml4
247:info:build CAMLP4DEPS plugins/subtac/g_subtac.ml4
248:info:build CAMLP4DEPS plugins/setoid_ring/newring.ml4
249:info:build CAMLP4DEPS plugins/rtauto/g_rtauto.ml4
250:info:build CAMLP4DEPS plugins/romega/g_romega.ml4
251:info:build CAMLP4DEPS plugins/ring/g_ring.ml4
252:info:build CAMLP4DEPS plugins/quote/g_quote.ml4
253:info:build CAMLP4DEPS plugins/omega/g_omega.ml4
254:info:build CAMLP4DEPS plugins/nsatz/nsatz.ml4
255:info:build CAMLP4DEPS plugins/micromega/g_micromega.ml4
256:info:build CAMLP4DEPS plugins/funind/g_indfun.ml4
257:info:build CAMLP4DEPS plugins/fourier/g_fourier.ml4
258:info:build CAMLP4DEPS plugins/firstorder/g_ground.ml4
259:info:build CAMLP4DEPS plugins/field/field.ml4
260:info:build CAMLP4DEPS plugins/extraction/g_extraction.ml4
261:info:build CAMLP4DEPS plugins/decl_mode/g_decl_mode.ml4
262:info:build CAMLP4DEPS plugins/cc/g_congruence.ml4
263:info:build CAMLP4DEPS parsing/vernacextend.ml4
264:info:build CAMLP4DEPS parsing/tacextend.ml4
265:info:build CAMLP4DEPS parsing/q_util.ml4
266:info:build CAMLP4DEPS parsing/q_coqast.ml4
267:info:build CAMLP4DEPS parsing/q_constr.ml4
268:info:build CAMLP4DEPS parsing/pcoq.ml4
269:info:build CAMLP4DEPS parsing/lexer.ml4
270:info:build CAMLP4DEPS parsing/g_xml.ml4
271:info:build CAMLP4DEPS parsing/g_vernac.ml4
272:info:build CAMLP4DEPS parsing/g_tactic.ml4
273:info:build CAMLP4DEPS parsing/g_proofs.ml4
274:info:build CAMLP4DEPS parsing/g_prim.ml4
275:info:build CAMLP4DEPS parsing/g_ltac.ml4
276:info:build CAMLP4DEPS parsing/g_constr.ml4
277:info:build CAMLP4DEPS parsing/argextend.ml4
278:info:build CAMLP4DEPS lib/pp.ml4
279:info:build CAMLP4DEPS lib/compat.ml4
280:info:build CAMLP4DEPS ide/project_file.ml4
281:info:build CAMLP4O   ide/coqide_main.ml4
282:info:build 454 states, 31913 transitions, table size 130376 bytes
283:info:build CAMLP4DEPS toplevel/mltop.ml4
284:info:build CAMLP4DEPS ide/coqide_main.ml4
285:info:build OCAMLBEST -o bin/coqdep_boot
286:info:build 2472 states, 7945 transitions, table size 46612 bytes
287:info:build File "tools/coqdep_common.ml", line 268, characters 17-19:
288:info:build Warning 3: deprecated: Pervasives.or
289:info:build Use (||) instead.
290:info:build File "tools/coqdep_common.ml", line 268, characters 28-30:
291:info:build Warning 3: deprecated: Pervasives.or
292:info:build Use (||) instead.
293:info:build File "tools/coqdep_common.ml", line 269, characters 1-3:
294:info:build Warning 3: deprecated: Pervasives.or
295:info:build Use (||) instead.
296:info:build File "tools/coqdep_common.ml", line 270, characters 1-3:
297:info:build Warning 3: deprecated: Pervasives.or
298:info:build Use (||) instead.
299:info:build File "tools/coqdep_common.ml", line 270, characters 12-14:
300:info:build Warning 3: deprecated: Pervasives.or
301:info:build Use (||) instead.
302:info:build File "tools/coqdep_common.ml", line 270, characters 23-25:
303:info:build Warning 3: deprecated: Pervasives.or
304:info:build Use (||) instead.
305:info:build File "tools/coqdep_common.ml", line 270, characters 34-36:
306:info:build Warning 3: deprecated: Pervasives.or
307:info:build Use (||) instead.
308:info:build File "tools/coqdep_common.ml", line 271, characters 1-3:
309:info:build Warning 3: deprecated: Pervasives.or
310:info:build Use (||) instead.
311:info:build OCAMLDEP  toplevel/whelp.mli
312:info:build OCAMLDEP  toplevel/vernacinterp.mli
313:info:build OCAMLDEP  toplevel/vernac.mli
314:info:build OCAMLDEP  toplevel/vernacentries.mli
315:info:build OCAMLDEP  toplevel/usage.mli
316:info:build OCAMLDEP  toplevel/toplevel.mli
317:info:build OCAMLDEP  toplevel/search.mli
318:info:build OCAMLDEP  toplevel/record.mli
319:info:build OCAMLDEP  toplevel/mltop.mli
320:info:build OCAMLDEP  toplevel/metasyntax.mli
321:info:build OCAMLDEP  toplevel/libtypes.mli
322:info:build OCAMLDEP  toplevel/lemmas.mli
323:info:build OCAMLDEP  toplevel/interface.mli
324:info:build OCAMLDEP  toplevel/indschemes.mli
325:info:build OCAMLDEP  toplevel/ind_tables.mli
326:info:build OCAMLDEP  toplevel/ide_slave.mli
327:info:build OCAMLDEP  toplevel/ide_intf.mli
328:info:build OCAMLDEP  toplevel/himsg.mli
329:info:build OCAMLDEP  toplevel/discharge.mli
330:info:build OCAMLDEP  toplevel/coqtop.mli
331:info:build OCAMLDEP  toplevel/coqinit.mli
332:info:build OCAMLDEP  toplevel/command.mli
333:info:build OCAMLDEP  toplevel/classes.mli
334:info:build OCAMLDEP  toplevel/class.mli
335:info:build OCAMLDEP  toplevel/cerrors.mli
336:info:build OCAMLDEP  toplevel/backtrack.mli
337:info:build OCAMLDEP  toplevel/autoinstance.mli
338:info:build OCAMLDEP  toplevel/auto_ind_decl.mli
339:info:build OCAMLDEP  tools/coqdoc/tokens.mli
340:info:build OCAMLDEP  tools/coqdoc/output.mli
341:info:build OCAMLDEP  tools/coqdoc/index.mli
342:info:build OCAMLDEP  tools/coqdoc/cpretty.mli
343:info:build OCAMLDEP  tools/coqdoc/alpha.mli
344:info:build OCAMLDEP  tools/coqdep_lexer.mli
345:info:build OCAMLDEP  tools/coqdep_common.mli
346:info:build OCAMLDEP  tactics/termdn.mli
347:info:build OCAMLDEP  tactics/tactics.mli
348:info:build OCAMLDEP  tactics/tacticals.mli
349:info:build OCAMLDEP  tactics/tactic_option.mli
350:info:build OCAMLDEP  tactics/tacinterp.mli
351:info:build OCAMLDEP  tactics/refine.mli
352:info:build OCAMLDEP  tactics/nbtermdn.mli
353:info:build OCAMLDEP  tactics/leminv.mli
354:info:build OCAMLDEP  tactics/inv.mli
355:info:build OCAMLDEP  tactics/hipattern.mli
356:info:build OCAMLDEP  tactics/hiddentac.mli
357:info:build OCAMLDEP  tactics/extratactics.mli
358:info:build OCAMLDEP  tactics/extraargs.mli
359:info:build OCAMLDEP  tactics/evar_tactics.mli
360:info:build OCAMLDEP  tactics/equality.mli
361:info:build OCAMLDEP  tactics/eqschemes.mli
362:info:build OCAMLDEP  tactics/elimschemes.mli
363:info:build OCAMLDEP  tactics/elim.mli
364:info:build OCAMLDEP  tactics/eauto.mli
365:info:build OCAMLDEP  tactics/dn.mli
366:info:build OCAMLDEP  tactics/contradiction.mli
367:info:build OCAMLDEP  tactics/btermdn.mli
368:info:build OCAMLDEP  tactics/autorewrite.mli
369:info:build OCAMLDEP  tactics/auto.mli
370:info:build OCAMLDEP  proofs/tactic_debug.mli
371:info:build OCAMLDEP  proofs/tacmach.mli
372:info:build OCAMLDEP  proofs/refiner.mli
373:info:build OCAMLDEP  proofs/redexpr.mli
374:info:build OCAMLDEP  proofs/proofview.mli
375:info:build OCAMLDEP  proofs/proof_type.mli
376:info:build OCAMLDEP  proofs/proof_global.mli
377:info:build OCAMLDEP  proofs/proof.mli
378:info:build OCAMLDEP  proofs/pfedit.mli
379:info:build OCAMLDEP  proofs/logic.mli
380:info:build OCAMLDEP  proofs/goal.mli
381:info:build OCAMLDEP  proofs/evar_refiner.mli
382:info:build OCAMLDEP  proofs/clenvtac.mli
383:info:build OCAMLDEP  proofs/clenv.mli
384:info:build OCAMLDEP  pretyping/vnorm.mli
385:info:build OCAMLDEP  pretyping/unification.mli
386:info:build OCAMLDEP  pretyping/typing.mli
387:info:build OCAMLDEP  pretyping/typeclasses_errors.mli
388:info:build OCAMLDEP  pretyping/typeclasses.mli
389:info:build OCAMLDEP  pretyping/termops.mli
390:info:build OCAMLDEP  pretyping/term_dnet.mli
391:info:build OCAMLDEP  pretyping/tacred.mli
392:info:build OCAMLDEP  pretyping/retyping.mli
393:info:build OCAMLDEP  pretyping/reductionops.mli
394:info:build OCAMLDEP  pretyping/recordops.mli
395:info:build OCAMLDEP  pretyping/pretyping.mli
396:info:build OCAMLDEP  pretyping/pretype_errors.mli
397:info:build OCAMLDEP  pretyping/pattern.mli
398:info:build OCAMLDEP  pretyping/namegen.mli
399:info:build OCAMLDEP  pretyping/matching.mli
400:info:build OCAMLDEP  pretyping/inductiveops.mli
401:info:build OCAMLDEP  pretyping/indrec.mli
402:info:build OCAMLDEP  pretyping/glob_term.mli
403:info:build OCAMLDEP  pretyping/evd.mli
404:info:build OCAMLDEP  pretyping/evarutil.mli
405:info:build OCAMLDEP  pretyping/evarconv.mli
406:info:build OCAMLDEP  pretyping/detyping.mli
407:info:build OCAMLDEP  pretyping/coercion.mli
408:info:build OCAMLDEP  pretyping/classops.mli
409:info:build OCAMLDEP  pretyping/cbv.mli
410:info:build OCAMLDEP  pretyping/cases.mli
411:info:build OCAMLDEP  pretyping/arguments_renaming.mli
412:info:build OCAMLDEP  plugins/xml/xmlcommand.mli
413:info:build OCAMLDEP  plugins/xml/xml.mli
414:info:build OCAMLDEP  plugins/xml/unshare.mli
415:info:build OCAMLDEP  plugins/xml/doubleTypeInference.mli
416:info:build OCAMLDEP  plugins/subtac/subtac_utils.mli
417:info:build OCAMLDEP  plugins/subtac/subtac_pretyping.mli
418:info:build OCAMLDEP  plugins/subtac/subtac_obligations.mli
419:info:build OCAMLDEP  plugins/subtac/subtac_errors.mli
420:info:build OCAMLDEP  plugins/subtac/subtac_command.mli
421:info:build OCAMLDEP  plugins/subtac/subtac_coercion.mli
422:info:build OCAMLDEP  plugins/subtac/subtac_classes.mli
423:info:build OCAMLDEP  plugins/subtac/subtac_cases.mli
424:info:build OCAMLDEP  plugins/subtac/subtac.mli
425:info:build OCAMLDEP  plugins/subtac/eterm.mli
426:info:build OCAMLDEP  plugins/rtauto/refl_tauto.mli
427:info:build OCAMLDEP  plugins/rtauto/proof_search.mli
428:info:build OCAMLDEP  plugins/romega/const_omega.mli
429:info:build OCAMLDEP  plugins/nsatz/utile.mli
430:info:build OCAMLDEP  plugins/nsatz/polynom.mli
431:info:build OCAMLDEP  plugins/micromega/sos.mli
432:info:build OCAMLDEP  plugins/micromega/micromega.mli
433:info:build OCAMLDEP  plugins/funind/indfun_common.mli
434:info:build OCAMLDEP  plugins/funind/indfun.mli
435:info:build OCAMLDEP  plugins/funind/glob_termops.mli
436:info:build OCAMLDEP  plugins/funind/glob_term_to_relation.mli
437:info:build OCAMLDEP  plugins/funind/functional_principles_types.mli
438:info:build OCAMLDEP  plugins/funind/functional_principles_proofs.mli
439:info:build OCAMLDEP  plugins/firstorder/unify.mli
440:info:build OCAMLDEP  plugins/firstorder/sequent.mli
441:info:build OCAMLDEP  plugins/firstorder/rules.mli
442:info:build OCAMLDEP  plugins/firstorder/instances.mli
443:info:build OCAMLDEP  plugins/firstorder/ground.mli
444:info:build OCAMLDEP  plugins/firstorder/formula.mli
445:info:build OCAMLDEP  plugins/extraction/table.mli
446:info:build OCAMLDEP  plugins/extraction/scheme.mli
447:info:build OCAMLDEP  plugins/extraction/ocaml.mli
448:info:build OCAMLDEP  plugins/extraction/modutil.mli
449:info:build OCAMLDEP  plugins/extraction/mlutil.mli
450:info:build OCAMLDEP  plugins/extraction/miniml.mli
451:info:build OCAMLDEP  plugins/extraction/haskell.mli
452:info:build OCAMLDEP  plugins/extraction/extraction.mli
453:info:build OCAMLDEP  plugins/extraction/extract_env.mli
454:info:build OCAMLDEP  plugins/extraction/common.mli
455:info:build OCAMLDEP  plugins/decl_mode/ppdecl_proof.mli
456:info:build OCAMLDEP  plugins/decl_mode/decl_proof_instr.mli
457:info:build OCAMLDEP  plugins/decl_mode/decl_mode.mli
458:info:build OCAMLDEP  plugins/decl_mode/decl_interp.mli
459:info:build OCAMLDEP  plugins/decl_mode/decl_expr.mli
460:info:build OCAMLDEP  plugins/cc/cctac.mli
461:info:build OCAMLDEP  plugins/cc/ccproof.mli
462:info:build OCAMLDEP  plugins/cc/ccalgo.mli
463:info:build OCAMLDEP  parsing/tok.mli
464:info:build OCAMLDEP  parsing/tactic_printer.mli
465:info:build OCAMLDEP  parsing/q_util.mli
466:info:build OCAMLDEP  parsing/printmod.mli
467:info:build OCAMLDEP  parsing/printer.mli
468:info:build OCAMLDEP  parsing/prettyp.mli
469:info:build OCAMLDEP  parsing/ppvernac.mli
470:info:build OCAMLDEP  parsing/pptactic.mli
471:info:build OCAMLDEP  parsing/ppconstr.mli
472:info:build OCAMLDEP  parsing/pcoq.mli
473:info:build OCAMLDEP  parsing/lexer.mli
474:info:build OCAMLDEP  parsing/extrawit.mli
475:info:build OCAMLDEP  parsing/extend.mli
476:info:build OCAMLDEP  parsing/egrammar.mli
477:info:build OCAMLDEP  library/summary.mli
478:info:build OCAMLDEP  library/states.mli
479:info:build OCAMLDEP  library/nametab.mli
480:info:build OCAMLDEP  library/nameops.mli
481:info:build OCAMLDEP  library/library.mli
482:info:build OCAMLDEP  library/libobject.mli
483:info:build OCAMLDEP  library/libnames.mli
484:info:build OCAMLDEP  library/lib.mli
485:info:build OCAMLDEP  library/impargs.mli
486:info:build OCAMLDEP  library/heads.mli
487:info:build OCAMLDEP  library/goptionstyp.mli
488:info:build OCAMLDEP  library/goptions.mli
489:info:build OCAMLDEP  library/global.mli
490:info:build OCAMLDEP  library/dischargedhypsmap.mli
491:info:build OCAMLDEP  library/decls.mli
492:info:build OCAMLDEP  library/declaremods.mli
493:info:build OCAMLDEP  library/declare.mli
494:info:build OCAMLDEP  library/decl_kinds.mli
495:info:build OCAMLDEP  library/assumptions.mli
496:info:build OCAMLDEP  lib/xml_utils.mli
497:info:build OCAMLDEP  lib/xml_parser.mli
498:info:build OCAMLDEP  lib/xml_lexer.mli
499:info:build OCAMLDEP  lib/util.mli
500:info:build OCAMLDEP  lib/unionfind.mli
501:info:build OCAMLDEP  lib/tries.mli
502:info:build OCAMLDEP  lib/system.mli
503:info:build OCAMLDEP  lib/store.mli
504:info:build OCAMLDEP  lib/segmenttree.mli
505:info:build OCAMLDEP  lib/rtree.mli
506:info:build OCAMLDEP  lib/profile.mli
507:info:build OCAMLDEP  lib/predicate.mli
508:info:build OCAMLDEP  lib/pp_control.mli
509:info:build OCAMLDEP  lib/pp.mli
510:info:build OCAMLDEP  lib/option.mli
511:info:build OCAMLDEP  lib/heap.mli
512:info:build OCAMLDEP  lib/hashtbl_alt.mli
513:info:build OCAMLDEP  lib/hashcons.mli
514:info:build OCAMLDEP  lib/gmapl.mli
515:info:build OCAMLDEP  lib/gmap.mli
516:info:build OCAMLDEP  lib/fset.mli
517:info:build OCAMLDEP  lib/fmap.mli
518:info:build OCAMLDEP  lib/flags.mli
519:info:build OCAMLDEP  lib/explore.mli
520:info:build OCAMLDEP  lib/errors.mli
521:info:build OCAMLDEP  lib/envars.mli
522:info:build OCAMLDEP  lib/dyn.mli
523:info:build OCAMLDEP  lib/dnet.mli
524:info:build OCAMLDEP  lib/bigint.mli
525:info:build OCAMLDEP  kernel/vm.mli
526:info:build OCAMLDEP  kernel/vconv.mli
527:info:build OCAMLDEP  kernel/univ.mli
528:info:build OCAMLDEP  kernel/typeops.mli
529:info:build OCAMLDEP  kernel/type_errors.mli
530:info:build OCAMLDEP  kernel/term_typing.mli
531:info:build OCAMLDEP  kernel/term.mli
532:info:build OCAMLDEP  kernel/subtyping.mli
533:info:build OCAMLDEP  kernel/sign.mli
534:info:build OCAMLDEP  kernel/safe_typing.mli
535:info:build OCAMLDEP  kernel/retroknowledge.mli
536:info:build OCAMLDEP  kernel/reduction.mli
537:info:build OCAMLDEP  kernel/pre_env.mli
538:info:build OCAMLDEP  kernel/names.mli
539:info:build OCAMLDEP  kernel/modops.mli
540:info:build OCAMLDEP  kernel/mod_typing.mli
541:info:build OCAMLDEP  kernel/mod_subst.mli
542:info:build OCAMLDEP  kernel/inductive.mli
543:info:build OCAMLDEP  kernel/indtypes.mli
544:info:build OCAMLDEP  kernel/esubst.mli
545:info:build OCAMLDEP  kernel/environ.mli
546:info:build OCAMLDEP  kernel/entries.mli
547:info:build OCAMLDEP  kernel/declarations.mli
548:info:build OCAMLDEP  kernel/csymtable.mli
549:info:build OCAMLDEP  kernel/cooking.mli
550:info:build OCAMLDEP  kernel/conv_oracle.mli
551:info:build OCAMLDEP  kernel/closure.mli
552:info:build OCAMLDEP  kernel/cemitcodes.mli
553:info:build OCAMLDEP  kernel/cbytegen.mli
554:info:build OCAMLDEP  kernel/cbytecodes.mli
555:info:build OCAMLDEP  interp/topconstr.mli
556:info:build OCAMLDEP  interp/syntax_def.mli
557:info:build OCAMLDEP  interp/smartlocate.mli
558:info:build OCAMLDEP  interp/reserve.mli
559:info:build OCAMLDEP  interp/ppextend.mli
560:info:build OCAMLDEP  interp/notation.mli
561:info:build OCAMLDEP  interp/modintern.mli
562:info:build OCAMLDEP  interp/implicit_quantifiers.mli
563:info:build OCAMLDEP  interp/genarg.mli
564:info:build OCAMLDEP  interp/dumpglob.mli
565:info:build OCAMLDEP  interp/coqlib.mli
566:info:build OCAMLDEP  interp/constrintern.mli
567:info:build OCAMLDEP  interp/constrextern.mli
568:info:build OCAMLDEP  ide/utils/okey.mli
569:info:build OCAMLDEP  ide/utils/configwin.mli
570:info:build OCAMLDEP  ide/utils/config_file.mli
571:info:build OCAMLDEP  ide/undo_lablgtk_lt26.mli
572:info:build OCAMLDEP  ide/undo_lablgtk_ge26.mli
573:info:build OCAMLDEP  ide/undo_lablgtk_ge212.mli
574:info:build OCAMLDEP  ide/tags.mli
575:info:build OCAMLDEP  ide/preferences.mli
576:info:build OCAMLDEP  ide/minilib.mli
577:info:build OCAMLDEP  ide/ideutils.mli
578:info:build OCAMLDEP  ide/coqide.mli
579:info:build OCAMLDEP  ide/coq.mli
580:info:build OCAMLDEP  ide/command_windows.mli
581:info:build OCAMLDEP  config/coq_config.mli
582:info:build OCAMLDEP  checker/typeops.mli
583:info:build OCAMLDEP  checker/type_errors.mli
584:info:build OCAMLDEP  checker/term.mli
585:info:build OCAMLDEP  checker/subtyping.mli
586:info:build OCAMLDEP  checker/safe_typing.mli
587:info:build OCAMLDEP  checker/reduction.mli
588:info:build OCAMLDEP  checker/modops.mli
589:info:build OCAMLDEP  checker/mod_checking.mli
590:info:build OCAMLDEP  checker/inductive.mli
591:info:build OCAMLDEP  checker/indtypes.mli
592:info:build OCAMLDEP  checker/environ.mli
593:info:build OCAMLDEP  checker/declarations.mli
594:info:build OCAMLDEP  checker/closure.mli
595:info:build OCAMLDEP  checker/check_stat.mli
596:info:build OCAMLDEP  plugins/xml/xml_plugin_mod.ml
597:info:build OCAMLDEP  plugins/syntax/z_syntax_plugin_mod.ml
598:info:build OCAMLDEP  plugins/syntax/string_syntax_plugin_mod.ml
599:info:build OCAMLDEP  plugins/syntax/r_syntax_plugin_mod.ml
600:info:build OCAMLDEP  plugins/syntax/numbers_syntax_plugin_mod.ml
601:info:build OCAMLDEP  plugins/syntax/nat_syntax_plugin_mod.ml
602:info:build OCAMLDEP  plugins/syntax/ascii_syntax_plugin_mod.ml
603:info:build OCAMLDEP  plugins/subtac/subtac_plugin_mod.ml
604:info:build OCAMLDEP  plugins/setoid_ring/newring_plugin_mod.ml
605:info:build OCAMLDEP  plugins/rtauto/rtauto_plugin_mod.ml
606:info:build OCAMLDEP  plugins/romega/romega_plugin_mod.ml
607:info:build OCAMLDEP  plugins/ring/ring_plugin_mod.ml
608:info:build OCAMLDEP  plugins/quote/quote_plugin_mod.ml
609:info:build OCAMLDEP  plugins/omega/omega_plugin_mod.ml
610:info:build OCAMLDEP  plugins/nsatz/nsatz_plugin_mod.ml
611:info:build OCAMLDEP  plugins/micromega/micromega_plugin_mod.ml
612:info:build OCAMLDEP  plugins/funind/recdef_plugin_mod.ml
613:info:build OCAMLDEP  plugins/fourier/fourier_plugin_mod.ml
614:info:build OCAMLDEP  plugins/firstorder/ground_plugin_mod.ml
615:info:build OCAMLDEP  plugins/field/field_plugin_mod.ml
616:info:build OCAMLDEP  plugins/extraction/extraction_plugin_mod.ml
617:info:build OCAMLDEP  plugins/decl_mode/decl_mode_plugin_mod.ml
618:info:build OCAMLDEP  plugins/cc/cc_plugin_mod.ml
619:info:build CAMLP4O   toplevel/whelp.ml4
620:info:build toplevel/whelp.ml4 : Dependency parsing/grammar.cma not ready yet
621:info:build OCAMLDEP  toplevel/mltop.ml
622:info:build CAMLP4O   tactics/tauto.ml4
623:info:build CAMLP4O   tactics/rewrite.ml4
624:info:build CAMLP4O   tactics/hipattern.ml4
625:info:build tactics/tauto.ml4 : Dependency parsing/grammar.cma not ready yet
626:info:build tactics/rewrite.ml4 : Dependency parsing/grammar.cma not ready yet
627:info:build CAMLP4O   tactics/extratactics.ml4
628:info:build tactics/hipattern.ml4 : Dependency parsing/grammar.cma parsing/q_constr.cmo not ready yet
629:info:build CAMLP4O   tactics/extraargs.ml4
630:info:build CAMLP4O   tactics/eqdecide.ml4
631:info:build tactics/extratactics.ml4 : Dependency parsing/grammar.cma not ready yet
632:info:build tactics/extraargs.ml4 : Dependency parsing/grammar.cma not ready yet
633:info:build CAMLP4O   tactics/eauto.ml4
634:info:build tactics/eqdecide.ml4 : Dependency parsing/grammar.cma not ready yet
635:info:build CAMLP4O   tactics/class_tactics.ml4
636:info:build CAMLP4O   plugins/xml/xmlentries.ml4
637:info:build tactics/eauto.ml4 : Dependency parsing/grammar.cma not ready yet
638:info:build tactics/class_tactics.ml4 : Dependency parsing/grammar.cma not ready yet
639:info:build CAMLP4O   plugins/xml/xml.ml4
640:info:build plugins/xml/xmlentries.ml4 : Dependency parsing/grammar.cma not ready yet
641:info:build CAMLP4O   plugins/xml/proofTree2Xml.ml4
642:info:build CAMLP4O   plugins/xml/dumptree.ml4
643:info:build CAMLP4O   plugins/xml/acic2Xml.ml4
644:info:build plugins/xml/dumptree.ml4 : Dependency parsing/grammar.cma not ready yet
645:info:build CAMLP4O   plugins/subtac/g_subtac.ml4
646:info:build Error while loading "tools/compat5.cmo": interface mismatch on CamlinternalFormatBasics.
647:info:build Error while loading "tools/compat5.cmo": interface mismatch on CamlinternalFormatBasics.
648:info:build Error while loading "tools/compat5.cmo": interface mismatch on CamlinternalFormatBasics.
649:info:build CAMLP4O   plugins/setoid_ring/newring.ml4
650:info:build CAMLP4O   plugins/rtauto/g_rtauto.ml4
651:info:build plugins/subtac/g_subtac.ml4 : Dependency parsing/grammar.cma not ready yet
652:info:build CAMLP4O   plugins/romega/g_romega.ml4
653:info:build CAMLP4O   plugins/ring/g_ring.ml4
654:info:build plugins/setoid_ring/newring.ml4 : Dependency parsing/grammar.cma not ready yet
655:info:build plugins/rtauto/g_rtauto.ml4 : Dependency parsing/grammar.cma not ready yet
656:info:build plugins/romega/g_romega.ml4 : Dependency parsing/grammar.cma not ready yet
657:info:build CAMLP4O   plugins/quote/g_quote.ml4
658:info:build CAMLP4O   plugins/omega/g_omega.ml4
659:info:build plugins/ring/g_ring.ml4 : Dependency parsing/grammar.cma not ready yet
660:info:build CAMLP4O   plugins/nsatz/nsatz.ml4
661:info:build CAMLP4O   plugins/micromega/g_micromega.ml4
662:info:build plugins/quote/g_quote.ml4 : Dependency parsing/grammar.cma not ready yet
663:info:build plugins/omega/g_omega.ml4 : Dependency parsing/grammar.cma not ready yet
664:info:build plugins/nsatz/nsatz.ml4 : Dependency parsing/grammar.cma not ready yet
665:info:build CAMLP4O   plugins/funind/g_indfun.ml4
666:info:build CAMLP4O   plugins/fourier/g_fourier.ml4
667:info:build plugins/micromega/g_micromega.ml4 : Dependency parsing/grammar.cma not ready yet
668:info:build CAMLP4O   plugins/firstorder/g_ground.ml4
669:info:build CAMLP4O   plugins/field/field.ml4
670:info:build plugins/fourier/g_fourier.ml4 : Dependency parsing/grammar.cma not ready yet
671:info:build plugins/funind/g_indfun.ml4 : Dependency parsing/grammar.cma not ready yet
672:info:build plugins/firstorder/g_ground.ml4 : Dependency parsing/grammar.cma not ready yet
673:info:build CAMLP4O   plugins/extraction/g_extraction.ml4
674:info:build plugins/field/field.ml4 : Dependency parsing/grammar.cma not ready yet
675:info:build CAMLP4O   plugins/decl_mode/g_decl_mode.ml4
676:info:build CAMLP4O   plugins/cc/g_congruence.ml4
677:info:build CAMLP4O   parsing/vernacextend.ml4
678:info:build plugins/extraction/g_extraction.ml4 : Dependency parsing/grammar.cma not ready yet
679:info:build plugins/decl_mode/g_decl_mode.ml4 : Dependency parsing/grammar.cma not ready yet
680:info:build plugins/cc/g_congruence.ml4 : Dependency parsing/grammar.cma not ready yet
681:info:build CAMLP4O   parsing/tacextend.ml4
682:info:build CAMLP4O   parsing/q_util.ml4
683:info:build CAMLP4O   parsing/q_coqast.ml4
684:info:build Error while loading "tools/compat5.cmo": interface mismatch on CamlinternalFormatBasics.
685:info:build CAMLP4O   parsing/q_constr.ml4
686:info:build Error while loading "tools/compat5.cmo": interface mismatch on CamlinternalFormatBasics.
687:info:build Error while loading "tools/compat5.cmo": interface mismatch on CamlinternalFormatBasics.
688:info:build Error while loading "tools/compat5.cmo": interface mismatch on CamlinternalFormatBasics.
689:info:build CAMLP4O   parsing/pcoq.ml4
690:info:build CAMLP4O   parsing/lexer.ml4
691:info:build CAMLP4O   parsing/g_xml.ml4
692:info:build Error while loading "tools/compat5.cmo": interface mismatch on CamlinternalFormatBasics.
693:info:build CAMLP4O   parsing/g_vernac.ml4
694:info:build Error while loading "tools/compat5.cmo": interface mismatch on CamlinternalFormatBasics.
695:info:build Error while loading "tools/compat5.cmo": interface mismatch on CamlinternalFormatBasics.
696:info:build Error while loading "tools/compat5.cmo": interface mismatch on CamlinternalFormatBasics.
697:info:build CAMLP4O   parsing/g_tactic.ml4
698:info:build CAMLP4O   parsing/g_proofs.ml4
699:info:build CAMLP4O   parsing/g_prim.ml4
700:info:build Error while loading "tools/compat5.cmo": interface mismatch on CamlinternalFormatBasics.
701:info:build CAMLP4O   parsing/g_ltac.ml4
702:info:build Error while loading "tools/compat5.cmo": interface mismatch on CamlinternalFormatBasics.
703:info:build Error while loading "tools/compat5.cmo": interface mismatch on CamlinternalFormatBasics.
704:info:build Error while loading "tools/compat5.cmo": interface mismatch on CamlinternalFormatBasics.
705:info:build CAMLP4O   parsing/g_constr.ml4
706:info:build CAMLP4O   parsing/argextend.ml4
707:info:build CAMLP4O   lib/pp.ml4
708:info:build Error while loading "tools/compat5.cmo": interface mismatch on CamlinternalFormatBasics.
709:info:build CAMLP4O   lib/compat.ml4
710:info:build Error while loading "tools/compat5.cmo": interface mismatch on CamlinternalFormatBasics.
711:info:build Error while loading "tools/compat5.cmo": interface mismatch on CamlinternalFormatBasics.
712:info:build Error while loading "tools/compat5.cmo": interface mismatch on CamlinternalFormatBasics.
713:info:build CAMLP4O   ide/project_file.ml4
714:info:build OCAMLDEP  ide/coqide_main.ml
715:info:build OCAMLDEP  kernel/copcodes.ml
716:info:build Error while loading "tools/compat5.cmo": interface mismatch on CamlinternalFormatBasics.
717:info:build OCAMLDEP  scripts/tolink.ml
718:info:build Error while loading "tools/compat5.cmo": interface mismatch on CamlinternalFormatBasics.
719:info:build OCAMLDEP  tools/gallina_lexer.ml
720:info:build OCAMLDEP  tools/coqwc.ml
721:info:build OCAMLDEP  tools/coqdoc/cpretty.ml
722:info:build OCAMLDEP  tools/coqdep_lexer.ml
723:info:build OCAMLDEP  lib/xml_lexer.ml
724:info:build OCAMLDEP  ide/utf8_convert.ml
725:info:build OCAMLDEP  ide/coq_lex.ml
726:info:build OCAMLDEP  ide/config_lexer.ml
727:info:build OCAMLDEP  toplevel/vernacinterp.ml
728:info:build OCAMLDEP  toplevel/vernacexpr.ml
729:info:build OCAMLDEP  toplevel/vernacentries.ml
730:info:build OCAMLDEP  toplevel/vernac.ml
731:info:build OCAMLDEP  toplevel/usage.ml
732:info:build OCAMLDEP  toplevel/toplevel.ml
733:info:build OCAMLDEP  toplevel/search.ml
734:info:build OCAMLDEP  toplevel/record.ml
735:info:build OCAMLDEP  toplevel/metasyntax.ml
736:info:build OCAMLDEP  toplevel/libtypes.ml
737:info:build OCAMLDEP  toplevel/lemmas.ml
738:info:build OCAMLDEP  toplevel/indschemes.ml
739:info:build OCAMLDEP  toplevel/ind_tables.ml
740:info:build OCAMLDEP  toplevel/ide_slave.ml
741:info:build OCAMLDEP  toplevel/ide_intf.ml
742:info:build OCAMLDEP  toplevel/himsg.ml
743:info:build OCAMLDEP  toplevel/discharge.ml
744:info:build OCAMLDEP  toplevel/coqtop.ml
745:info:build OCAMLDEP  toplevel/coqinit.ml
746:info:build OCAMLDEP  toplevel/command.ml
747:info:build OCAMLDEP  toplevel/classes.ml
748:info:build OCAMLDEP  toplevel/class.ml
749:info:build OCAMLDEP  toplevel/cerrors.ml
750:info:build OCAMLDEP  toplevel/backtrack.ml
751:info:build OCAMLDEP  toplevel/autoinstance.ml
752:info:build OCAMLDEP  toplevel/auto_ind_decl.ml
753:info:build OCAMLDEP  tools/win32hack_filename.ml
754:info:build OCAMLDEP  tools/mkwinapp.ml
755:info:build OCAMLDEP  tools/mingwpath.ml
756:info:build OCAMLDEP  tools/gallina.ml
757:info:build OCAMLDEP  tools/fake_ide.ml
758:info:build OCAMLDEP  tools/escape_string.ml
759:info:build OCAMLDEP  tools/coqdoc/tokens.ml
760:info:build OCAMLDEP  tools/coqdoc/output.ml
761:info:build OCAMLDEP  tools/coqdoc/main.ml
762:info:build OCAMLDEP  tools/coqdoc/index.ml
763:info:build OCAMLDEP  tools/coqdoc/cdglobals.ml
764:info:build OCAMLDEP  tools/coqdoc/alpha.ml
765:info:build OCAMLDEP  tools/coqdep_common.ml
766:info:build OCAMLDEP  tools/coqdep_boot.ml
767:info:build OCAMLDEP  tools/coqdep.ml
768:info:build OCAMLDEP  tools/coq_tex.ml
769:info:build OCAMLDEP  tools/coq_makefile.ml
770:info:build OCAMLDEP  tools/compat5b.ml
771:info:build OCAMLDEP  tools/compat5.ml
772:info:build OCAMLDEP  theories/Numbers/Natural/BigN/NMake_gen.ml
773:info:build OCAMLDEP  tactics/termdn.ml
774:info:build OCAMLDEP  tactics/tactics.ml
775:info:build OCAMLDEP  tactics/tacticals.ml
776:info:build OCAMLDEP  tactics/tactic_option.ml
777:info:build OCAMLDEP  tactics/tacinterp.ml
778:info:build OCAMLDEP  tactics/refine.ml
779:info:build OCAMLDEP  tactics/nbtermdn.ml
780:info:build OCAMLDEP  tactics/leminv.ml
781:info:build OCAMLDEP  tactics/inv.ml
782:info:build OCAMLDEP  tactics/hiddentac.ml
783:info:build OCAMLDEP  tactics/evar_tactics.ml
784:info:build OCAMLDEP  tactics/equality.ml
785:info:build OCAMLDEP  tactics/eqschemes.ml
786:info:build OCAMLDEP  tactics/elimschemes.ml
787:info:build OCAMLDEP  tactics/elim.ml
788:info:build OCAMLDEP  tactics/dn.ml
789:info:build OCAMLDEP  tactics/contradiction.ml
790:info:build OCAMLDEP  tactics/btermdn.ml
791:info:build OCAMLDEP  tactics/autorewrite.ml
792:info:build OCAMLDEP  tactics/auto.ml
793:info:build OCAMLDEP  scripts/coqmktop.ml
794:info:build OCAMLDEP  scripts/coqc.ml
795:info:build OCAMLDEP  proofs/tactic_debug.ml
796:info:build OCAMLDEP  proofs/tacmach.ml
797:info:build OCAMLDEP  proofs/tacexpr.ml
798:info:build OCAMLDEP  proofs/refiner.ml
799:info:build OCAMLDEP  proofs/redexpr.ml
800:info:build OCAMLDEP  proofs/proofview.ml
801:info:build OCAMLDEP  proofs/proof_type.ml
802:info:build OCAMLDEP  proofs/proof_global.ml
803:info:build OCAMLDEP  proofs/proof.ml
804:info:build OCAMLDEP  proofs/pfedit.ml
805:info:build OCAMLDEP  proofs/logic.ml
806:info:build OCAMLDEP  proofs/goal.ml
807:info:build OCAMLDEP  proofs/evar_refiner.ml
808:info:build OCAMLDEP  proofs/clenvtac.ml
809:info:build OCAMLDEP  proofs/clenv.ml
810:info:build OCAMLDEP  pretyping/vnorm.ml
811:info:build OCAMLDEP  pretyping/unification.ml
812:info:build OCAMLDEP  pretyping/typing.ml
813:info:build OCAMLDEP  pretyping/typeclasses_errors.ml
814:info:build OCAMLDEP  pretyping/typeclasses.ml
815:info:build OCAMLDEP  pretyping/termops.ml
816:info:build OCAMLDEP  pretyping/term_dnet.ml
817:info:build OCAMLDEP  pretyping/tacred.ml
818:info:build OCAMLDEP  pretyping/retyping.ml
819:info:build OCAMLDEP  pretyping/reductionops.ml
820:info:build OCAMLDEP  pretyping/recordops.ml
821:info:build OCAMLDEP  pretyping/pretyping.ml
822:info:build OCAMLDEP  pretyping/pretype_errors.ml
823:info:build OCAMLDEP  pretyping/pattern.ml
824:info:build OCAMLDEP  pretyping/namegen.ml
825:info:build OCAMLDEP  pretyping/matching.ml
826:info:build OCAMLDEP  pretyping/inductiveops.ml
827:info:build OCAMLDEP  pretyping/indrec.ml
828:info:build OCAMLDEP  pretyping/glob_term.ml
829:info:build OCAMLDEP  pretyping/evd.ml
830:info:build OCAMLDEP  pretyping/evarutil.ml
831:info:build OCAMLDEP  pretyping/evarconv.ml
832:info:build OCAMLDEP  pretyping/detyping.ml
833:info:build OCAMLDEP  pretyping/coercion.ml
834:info:build OCAMLDEP  pretyping/classops.ml
835:info:build OCAMLDEP  pretyping/cbv.ml
836:info:build OCAMLDEP  pretyping/cases.ml
837:info:build OCAMLDEP  pretyping/arguments_renaming.ml
838:info:build OCAMLDEP  plugins/xml/xmlcommand.ml
839:info:build OCAMLDEP  plugins/xml/unshare.ml
840:info:build OCAMLDEP  plugins/xml/proof2aproof.ml
841:info:build OCAMLDEP  plugins/xml/doubleTypeInference.ml
842:info:build OCAMLDEP  plugins/xml/cic2Xml.ml
843:info:build OCAMLDEP  plugins/xml/cic2acic.ml
844:info:build OCAMLDEP  plugins/xml/acic.ml
845:info:build OCAMLDEP  plugins/syntax/z_syntax.ml
846:info:build OCAMLDEP  plugins/syntax/string_syntax.ml
847:info:build OCAMLDEP  plugins/syntax/r_syntax.ml
848:info:build OCAMLDEP  plugins/syntax/numbers_syntax.ml
849:info:build OCAMLDEP  plugins/syntax/nat_syntax.ml
850:info:build OCAMLDEP  plugins/syntax/ascii_syntax.ml
851:info:build OCAMLDEP  plugins/subtac/subtac_utils.ml
852:info:build OCAMLDEP  plugins/subtac/subtac_pretyping_F.ml
853:info:build OCAMLDEP  plugins/subtac/subtac_pretyping.ml
854:info:build OCAMLDEP  plugins/subtac/subtac_obligations.ml
855:info:build OCAMLDEP  plugins/subtac/subtac_errors.ml
856:info:build OCAMLDEP  plugins/subtac/subtac_command.ml
857:info:build OCAMLDEP  plugins/subtac/subtac_coercion.ml
858:info:build OCAMLDEP  plugins/subtac/subtac_classes.ml
859:info:build OCAMLDEP  plugins/subtac/subtac_cases.ml
860:info:build OCAMLDEP  plugins/subtac/subtac.ml
861:info:build OCAMLDEP  plugins/subtac/eterm.ml
862:info:build OCAMLDEP  plugins/rtauto/refl_tauto.ml
863:info:build OCAMLDEP  plugins/rtauto/proof_search.ml
864:info:build OCAMLDEP  plugins/romega/refl_omega.ml
865:info:build OCAMLDEP  plugins/romega/const_omega.ml
866:info:build OCAMLDEP  plugins/ring/ring.ml
867:info:build OCAMLDEP  plugins/quote/quote.ml
868:info:build OCAMLDEP  plugins/omega/omega.ml
869:info:build OCAMLDEP  plugins/omega/coq_omega.ml
870:info:build OCAMLDEP  plugins/nsatz/utile.ml
871:info:build OCAMLDEP  plugins/nsatz/polynom.ml
872:info:build OCAMLDEP  plugins/nsatz/ideal.ml
873:info:build OCAMLDEP  plugins/micromega/sos_types.ml
874:info:build OCAMLDEP  plugins/micromega/sos_lib.ml
875:info:build OCAMLDEP  plugins/micromega/sos.ml
876:info:build OCAMLDEP  plugins/micromega/polynomial.ml
877:info:build OCAMLDEP  plugins/micromega/persistent_cache.ml
878:info:build OCAMLDEP  plugins/micromega/mutils.ml
879:info:build OCAMLDEP  plugins/micromega/micromega.ml
880:info:build OCAMLDEP  plugins/micromega/mfourier.ml
881:info:build OCAMLDEP  plugins/micromega/csdpcert.ml
882:info:build OCAMLDEP  plugins/micromega/coq_micromega.ml
883:info:build OCAMLDEP  plugins/micromega/certificate.ml
884:info:build OCAMLDEP  plugins/funind/recdef.ml
885:info:build OCAMLDEP  plugins/funind/merge.ml
886:info:build OCAMLDEP  plugins/funind/invfun.ml
887:info:build OCAMLDEP  plugins/funind/indfun_common.ml
888:info:build OCAMLDEP  plugins/funind/indfun.ml
889:info:build OCAMLDEP  plugins/funind/glob_termops.ml
890:info:build OCAMLDEP  plugins/funind/glob_term_to_relation.ml
891:info:build OCAMLDEP  plugins/funind/functional_principles_types.ml
892:info:build OCAMLDEP  plugins/funind/functional_principles_proofs.ml
893:info:build OCAMLDEP  plugins/fourier/fourierR.ml
894:info:build OCAMLDEP  plugins/fourier/fourier.ml
895:info:build OCAMLDEP  plugins/firstorder/unify.ml
896:info:build OCAMLDEP  plugins/firstorder/sequent.ml
897:info:build OCAMLDEP  plugins/firstorder/rules.ml
898:info:build OCAMLDEP  plugins/firstorder/instances.ml
899:info:build OCAMLDEP  plugins/firstorder/ground.ml
900:info:build OCAMLDEP  plugins/firstorder/formula.ml
901:info:build OCAMLDEP  plugins/extraction/table.ml
902:info:build OCAMLDEP  plugins/extraction/scheme.ml
903:info:build OCAMLDEP  plugins/extraction/ocaml.ml
904:info:build OCAMLDEP  plugins/extraction/modutil.ml
905:info:build OCAMLDEP  plugins/extraction/mlutil.ml
906:info:build OCAMLDEP  plugins/extraction/haskell.ml
907:info:build OCAMLDEP  plugins/extraction/extraction.ml
908:info:build OCAMLDEP  plugins/extraction/extract_env.ml
909:info:build OCAMLDEP  plugins/extraction/common.ml
910:info:build OCAMLDEP  plugins/extraction/big.ml
911:info:build OCAMLDEP  plugins/decl_mode/ppdecl_proof.ml
912:info:build OCAMLDEP  plugins/decl_mode/decl_proof_instr.ml
913:info:build OCAMLDEP  plugins/decl_mode/decl_mode.ml
914:info:build OCAMLDEP  plugins/decl_mode/decl_interp.ml
915:info:build OCAMLDEP  plugins/cc/cctac.ml
916:info:build OCAMLDEP  plugins/cc/ccproof.ml
917:info:build OCAMLDEP  plugins/cc/ccalgo.ml
918:info:build OCAMLDEP  parsing/tok.ml
919:info:build OCAMLDEP  parsing/tactic_printer.ml
920:info:build OCAMLDEP  parsing/printmod.ml
921:info:build OCAMLDEP  parsing/printer.ml
922:info:build OCAMLDEP  parsing/prettyp.ml
923:info:build OCAMLDEP  parsing/ppvernac.ml
924:info:build OCAMLDEP  parsing/pptactic.ml
925:info:build OCAMLDEP  parsing/ppconstr.ml
926:info:build OCAMLDEP  parsing/extrawit.ml
927:info:build OCAMLDEP  parsing/extend.ml
928:info:build OCAMLDEP  parsing/egrammar.ml
929:info:build OCAMLDEP  myocamlbuild.ml
930:info:build OCAMLDEP  library/summary.ml
931:info:build OCAMLDEP  library/states.ml
932:info:build OCAMLDEP  library/nametab.ml
933:info:build OCAMLDEP  library/nameops.ml
934:info:build OCAMLDEP  library/library.ml
935:info:build OCAMLDEP  library/libobject.ml
936:info:build OCAMLDEP  library/libnames.ml
937:info:build OCAMLDEP  library/lib.ml
938:info:build OCAMLDEP  library/impargs.ml
939:info:build OCAMLDEP  library/heads.ml
940:info:build OCAMLDEP  library/goptions.ml
941:info:build OCAMLDEP  library/global.ml
942:info:build OCAMLDEP  library/dischargedhypsmap.ml
943:info:build OCAMLDEP  library/decls.ml
944:info:build OCAMLDEP  library/declaremods.ml
945:info:build OCAMLDEP  library/declare.ml
946:info:build OCAMLDEP  library/decl_kinds.ml
947:info:build OCAMLDEP  library/assumptions.ml
948:info:build OCAMLDEP  lib/xml_utils.ml
949:info:build OCAMLDEP  lib/xml_parser.ml
950:info:build OCAMLDEP  lib/util.ml
951:info:build OCAMLDEP  lib/unionfind.ml
952:info:build OCAMLDEP  lib/unicodetable.ml
953:info:build OCAMLDEP  lib/tries.ml
954:info:build OCAMLDEP  lib/system.ml
955:info:build OCAMLDEP  lib/store.ml
956:info:build OCAMLDEP  lib/segmenttree.ml
957:info:build OCAMLDEP  lib/rtree.ml
958:info:build OCAMLDEP  lib/profile.ml
959:info:build OCAMLDEP  lib/predicate.ml
960:info:build OCAMLDEP  lib/pp_control.ml
961:info:build OCAMLDEP  lib/option.ml
962:info:build OCAMLDEP  lib/heap.ml
963:info:build OCAMLDEP  lib/hashtbl_alt.ml
964:info:build OCAMLDEP  lib/hashcons.ml
965:info:build OCAMLDEP  lib/gmapl.ml
966:info:build OCAMLDEP  lib/gmap.ml
967:info:build OCAMLDEP  lib/fset.ml
968:info:build OCAMLDEP  lib/fmap.ml
969:info:build OCAMLDEP  lib/flags.ml
970:info:build OCAMLDEP  lib/explore.ml
971:info:build OCAMLDEP  lib/errors.ml
972:info:build OCAMLDEP  lib/envars.ml
973:info:build OCAMLDEP  lib/dyn.ml
974:info:build OCAMLDEP  lib/dnet.ml
975:info:build OCAMLDEP  lib/bigint.ml
976:info:build OCAMLDEP  kernel/vm.ml
977:info:build OCAMLDEP  kernel/vconv.ml
978:info:build OCAMLDEP  kernel/univ.ml
979:info:build OCAMLDEP  kernel/typeops.ml
980:info:build OCAMLDEP  kernel/type_errors.ml
981:info:build OCAMLDEP  kernel/term_typing.ml
982:info:build OCAMLDEP  kernel/term.ml
983:info:build OCAMLDEP  kernel/subtyping.ml
984:info:build OCAMLDEP  kernel/sign.ml
985:info:build OCAMLDEP  kernel/safe_typing.ml
986:info:build OCAMLDEP  kernel/retroknowledge.ml
987:info:build OCAMLDEP  kernel/reduction.ml
988:info:build OCAMLDEP  kernel/pre_env.ml
989:info:build OCAMLDEP  kernel/names.ml
990:info:build OCAMLDEP  kernel/modops.ml
991:info:build OCAMLDEP  kernel/mod_typing.ml
992:info:build OCAMLDEP  kernel/mod_subst.ml
993:info:build OCAMLDEP  kernel/inductive.ml
994:info:build OCAMLDEP  kernel/indtypes.ml
995:info:build OCAMLDEP  kernel/esubst.ml
996:info:build OCAMLDEP  kernel/environ.ml
997:info:build OCAMLDEP  kernel/entries.ml
998:info:build OCAMLDEP  kernel/declarations.ml
999:info:build OCAMLDEP  kernel/csymtable.ml
1000:info:build OCAMLDEP  kernel/cooking.ml
1001:info:build OCAMLDEP  kernel/conv_oracle.ml
1002:info:build OCAMLDEP  kernel/closure.ml
1003:info:build OCAMLDEP  kernel/cemitcodes.ml
1004:info:build OCAMLDEP  kernel/cbytegen.ml
1005:info:build OCAMLDEP  kernel/cbytecodes.ml
1006:info:build OCAMLDEP  interp/topconstr.ml
1007:info:build OCAMLDEP  interp/syntax_def.ml
1008:info:build OCAMLDEP  interp/smartlocate.ml
1009:info:build OCAMLDEP  interp/reserve.ml
1010:info:build OCAMLDEP  interp/ppextend.ml
1011:info:build OCAMLDEP  interp/notation.ml
1012:info:build OCAMLDEP  interp/modintern.ml
1013:info:build OCAMLDEP  interp/implicit_quantifiers.ml
1014:info:build OCAMLDEP  interp/genarg.ml
1015:info:build OCAMLDEP  interp/dumpglob.ml
1016:info:build OCAMLDEP  interp/coqlib.ml
1017:info:build OCAMLDEP  interp/constrintern.ml
1018:info:build OCAMLDEP  interp/constrextern.ml
1019:info:build OCAMLDEP  ide/utils/okey.ml
1020:info:build OCAMLDEP  ide/utils/editable_cells.ml
1021:info:build OCAMLDEP  ide/utils/configwin_types.ml
1022:info:build OCAMLDEP  ide/utils/configwin_messages.ml
1023:info:build OCAMLDEP  ide/utils/configwin_keys.ml
1024:info:build OCAMLDEP  ide/utils/configwin_ihm.ml
1025:info:build OCAMLDEP  ide/utils/configwin.ml
1026:info:build OCAMLDEP  ide/utils/config_file.ml
1027:info:build OCAMLDEP  ide/undo.ml
1028:info:build OCAMLDEP  ide/typed_notebook.ml
1029:info:build OCAMLDEP  ide/tags.ml
1030:info:build OCAMLDEP  ide/preferences.ml
1031:info:build OCAMLDEP  ide/minilib.ml
1032:info:build OCAMLDEP  ide/ideutils.ml
1033:info:build OCAMLDEP  ide/ideproof.ml
1034:info:build OCAMLDEP  ide/gtk_parsing.ml
1035:info:build OCAMLDEP  ide/coqide_ui.ml
1036:info:build OCAMLDEP  ide/coqide.ml
1037:info:build OCAMLDEP  ide/coq_commands.ml
1038:info:build OCAMLDEP  ide/coq.ml
1039:info:build OCAMLDEP  ide/command_windows.ml
1040:info:build OCAMLDEP  dev/vm_printers.ml
1041:info:build OCAMLDEP  dev/top_printers.ml
1042:info:build OCAMLDEP  dev/db_printers.ml
1043:info:build OCAMLDEP  config/coq_config.ml
1044:info:build OCAMLDEP  checker/validate.ml
1045:info:build OCAMLDEP  checker/typeops.ml
1046:info:build OCAMLDEP  checker/type_errors.ml
1047:info:build OCAMLDEP  checker/term.ml
1048:info:build OCAMLDEP  checker/subtyping.ml
1049:info:build OCAMLDEP  checker/safe_typing.ml
1050:info:build OCAMLDEP  checker/reduction.ml
1051:info:build OCAMLDEP  checker/modops.ml
1052:info:build OCAMLDEP  checker/mod_checking.ml
1053:info:build OCAMLDEP  checker/main.ml
1054:info:build OCAMLDEP  checker/inductive.ml
1055:info:build OCAMLDEP  checker/indtypes.ml
1056:info:build OCAMLDEP  checker/environ.ml
1057:info:build OCAMLDEP  checker/declarations.ml
1058:info:build OCAMLDEP  checker/closure.ml
1059:info:build OCAMLDEP  checker/checker.ml
1060:info:build OCAMLDEP  checker/check_stat.ml
1061:info:build OCAMLDEP  checker/check.ml
1062:info:build COQDEP    plugins/extraction/ExtrOcamlZBigInt.v
1063:info:build COQDEP    plugins/extraction/ExtrOcamlString.v
1064:info:build COQDEP    plugins/extraction/ExtrOcamlZInt.v
1065:info:build COQDEP    plugins/extraction/ExtrOcamlNatBigInt.v
1066:info:build COQDEP    plugins/extraction/ExtrOcamlNatInt.v
1067:info:build COQDEP    plugins/extraction/ExtrOcamlBigIntConv.v
1068:info:build COQDEP    plugins/extraction/ExtrOcamlIntConv.v
1069:info:build COQDEP    plugins/extraction/ExtrOcamlBasic.v
1070:info:build COQDEP    plugins/nsatz/Nsatz.v
1071:info:build COQDEP    plugins/quote/Quote.v
1072:info:build COQDEP    plugins/setoid_ring/Integral_domain.v
1073:info:build COQDEP    plugins/setoid_ring/Rings_Q.v
1074:info:build COQDEP    plugins/setoid_ring/Rings_R.v
1075:info:build COQDEP    plugins/setoid_ring/Rings_Z.v
1076:info:build COQDEP    plugins/setoid_ring/Ncring_tac.v
1077:info:build COQDEP    plugins/setoid_ring/Ncring_initial.v
1078:info:build COQDEP    plugins/setoid_ring/Ncring_polynom.v
1079:info:build COQDEP    plugins/setoid_ring/Ncring.v
1080:info:build COQDEP    plugins/setoid_ring/Cring.v
1081:info:build COQDEP    plugins/setoid_ring/Algebra_syntax.v
1082:info:build COQDEP    plugins/setoid_ring/ZArithRing.v
1083:info:build COQDEP    plugins/setoid_ring/Ring.v
1084:info:build COQDEP    plugins/setoid_ring/Ring_theory.v
1085:info:build COQDEP    plugins/setoid_ring/Ring_tac.v
1086:info:build COQDEP    plugins/setoid_ring/Ring_polynom.v
1087:info:build COQDEP    plugins/setoid_ring/Ring_equiv.v
1088:info:build COQDEP    plugins/setoid_ring/Ring_base.v
1089:info:build COQDEP    plugins/setoid_ring/RealField.v
1090:info:build COQDEP    plugins/setoid_ring/NArithRing.v
1091:info:build COQDEP    plugins/setoid_ring/InitialRing.v
1092:info:build COQDEP    plugins/setoid_ring/Field.v
1093:info:build COQDEP    plugins/setoid_ring/Field_theory.v
1094:info:build COQDEP    plugins/setoid_ring/Field_tac.v
1095:info:build COQDEP    plugins/setoid_ring/BinList.v
1096:info:build COQDEP    plugins/setoid_ring/ArithRing.v
1097:info:build COQDEP    plugins/rtauto/Rtauto.v
1098:info:build COQDEP    plugins/rtauto/Bintree.v
1099:info:build COQDEP    plugins/funind/Recdef.v
1100:info:build COQDEP    plugins/fourier/Fourier.v
1101:info:build COQDEP    plugins/fourier/Fourier_util.v
1102:info:build COQDEP    plugins/field/LegacyField.v
1103:info:build COQDEP    plugins/field/LegacyField_Theory.v
1104:info:build COQDEP    plugins/field/LegacyField_Tactic.v
1105:info:build COQDEP    plugins/field/LegacyField_Compl.v
1106:info:build COQDEP    plugins/ring/Setoid_ring.v
1107:info:build COQDEP    plugins/ring/Setoid_ring_theory.v
1108:info:build COQDEP    plugins/ring/Setoid_ring_normalize.v
1109:info:build COQDEP    plugins/ring/Ring_normalize.v
1110:info:build COQDEP    plugins/ring/Ring_abstract.v
1111:info:build COQDEP    plugins/ring/LegacyZArithRing.v
1112:info:build COQDEP    plugins/ring/LegacyRing.v
1113:info:build COQDEP    plugins/ring/LegacyRing_theory.v
1114:info:build COQDEP    plugins/ring/LegacyNArithRing.v
1115:info:build COQDEP    plugins/ring/LegacyArithRing.v
1116:info:build COQDEP    plugins/micromega/ZMicromega.v
1117:info:build COQDEP    plugins/micromega/ZCoeff.v
1118:info:build COQDEP    plugins/micromega/VarMap.v
1119:info:build COQDEP    plugins/micromega/Tauto.v
1120:info:build COQDEP    plugins/micromega/RMicromega.v
1121:info:build COQDEP    plugins/micromega/RingMicromega.v
1122:info:build COQDEP    plugins/micromega/Refl.v
1123:info:build COQDEP    plugins/micromega/QMicromega.v
1124:info:build COQDEP    plugins/micromega/Psatz.v
1125:info:build COQDEP    plugins/micromega/OrderedRing.v
1126:info:build COQDEP    plugins/micromega/Env.v
1127:info:build COQDEP    plugins/micromega/EnvRing.v
1128:info:build COQDEP    plugins/micromega/CheckerMaker.v
1129:info:build COQDEP    plugins/romega/ROmega.v
1130:info:build COQDEP    plugins/romega/ReflOmegaCore.v
1131:info:build COQDEP    plugins/omega/PreOmega.v
1132:info:build COQDEP    plugins/omega/Omega.v
1133:info:build COQDEP    plugins/omega/OmegaPlugin.v
1134:info:build COQDEP    plugins/omega/OmegaLemmas.v
1135:info:build COQDEP    theories/Vectors/Vector.v
1136:info:build COQDEP    theories/Vectors/VectorSpec.v
1137:info:build COQDEP    theories/Vectors/VectorDef.v
1138:info:build COQDEP    theories/Vectors/Fin.v
1139:info:build COQDEP    theories/Structures/OrderedType.v
1140:info:build COQDEP    theories/Structures/OrderedTypeEx.v
1141:info:build COQDEP    theories/Structures/OrderedTypeAlt.v
1142:info:build COQDEP    theories/Structures/DecidableTypeEx.v
1143:info:build COQDEP    theories/Structures/DecidableType.v
1144:info:build COQDEP    theories/Structures/GenericMinMax.v
1145:info:build COQDEP    theories/Structures/OrdersAlt.v
1146:info:build COQDEP    theories/Structures/OrdersTac.v
1147:info:build COQDEP    theories/Structures/OrdersLists.v
1148:info:build COQDEP    theories/Structures/OrdersFacts.v
1149:info:build COQDEP    theories/Structures/OrdersEx.v
1150:info:build COQDEP    theories/Structures/Orders.v
1151:info:build COQDEP    theories/Structures/EqualitiesFacts.v
1152:info:build COQDEP    theories/Structures/Equalities.v
1153:info:build COQDEP    theories/Program/Wf.v
1154:info:build COQDEP    theories/Program/Utils.v
1155:info:build COQDEP    theories/Program/Tactics.v
1156:info:build COQDEP    theories/Program/Syntax.v
1157:info:build COQDEP    theories/Program/Subset.v
1158:info:build COQDEP    theories/Program/Program.v
1159:info:build COQDEP    theories/Program/Equality.v
1160:info:build COQDEP    theories/Program/Combinators.v
1161:info:build COQDEP    theories/Program/Basics.v
1162:info:build COQDEP    theories/Classes/RelationPairs.v
1163:info:build COQDEP    theories/Classes/SetoidTactics.v
1164:info:build COQDEP    theories/Classes/SetoidDec.v
1165:info:build COQDEP    theories/Classes/SetoidClass.v
1166:info:build COQDEP    theories/Classes/RelationClasses.v
1167:info:build COQDEP    theories/Classes/Morphisms.v
1168:info:build COQDEP    theories/Classes/Morphisms_Relations.v
1169:info:build COQDEP    theories/Classes/Morphisms_Prop.v
1170:info:build COQDEP    theories/Classes/Init.v
1171:info:build COQDEP    theories/Classes/EquivDec.v
1172:info:build COQDEP    theories/Classes/Equivalence.v
1173:info:build COQDEP    theories/Unicode/Utf8_core.v
1174:info:build COQDEP    theories/Unicode/Utf8.v
1175:info:build COQDEP    theories/Numbers/Rational/SpecViaQ/QSig.v
1176:info:build COQDEP    theories/Numbers/Rational/BigQ/QMake.v
1177:info:build COQDEP    theories/Numbers/Rational/BigQ/BigQ.v
1178:info:build COQDEP    theories/Numbers/NumPrelude.v
1179:info:build COQDEP    theories/Numbers/Natural/SpecViaZ/NSig.v
1180:info:build COQDEP    theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v
1181:info:build COQDEP    theories/Numbers/Natural/Peano/NPeano.v
1182:info:build COQDEP    theories/Numbers/Natural/Binary/NBinary.v
1183:info:build COQDEP    theories/Numbers/Natural/BigN/NMake.v
1184:info:build COQDEP    theories/Numbers/Natural/BigN/NMake_gen.v
1185:info:build COQDEP    theories/Numbers/Natural/BigN/Nbasic.v
1186:info:build COQDEP    theories/Numbers/Natural/BigN/BigN.v
1187:info:build COQDEP    theories/Numbers/Natural/Abstract/NBits.v
1188:info:build COQDEP    theories/Numbers/Natural/Abstract/NLcm.v
1189:info:build COQDEP    theories/Numbers/Natural/Abstract/NGcd.v
1190:info:build COQDEP    theories/Numbers/Natural/Abstract/NLog.v
1191:info:build COQDEP    theories/Numbers/Natural/Abstract/NSqrt.v
1192:info:build COQDEP    theories/Numbers/Natural/Abstract/NPow.v
1193:info:build COQDEP    theories/Numbers/Natural/Abstract/NParity.v
1194:info:build COQDEP    theories/Numbers/Natural/Abstract/NMaxMin.v
1195:info:build COQDEP    theories/Numbers/Natural/Abstract/NDiv.v
1196:info:build COQDEP    theories/Numbers/Natural/Abstract/NProperties.v
1197:info:build COQDEP    theories/Numbers/Natural/Abstract/NSub.v
1198:info:build COQDEP    theories/Numbers/Natural/Abstract/NStrongRec.v
1199:info:build COQDEP    theories/Numbers/Natural/Abstract/NOrder.v
1200:info:build COQDEP    theories/Numbers/Natural/Abstract/NMulOrder.v
1201:info:build COQDEP    theories/Numbers/Natural/Abstract/NIso.v
1202:info:build COQDEP    theories/Numbers/Natural/Abstract/NDefOps.v
1203:info:build COQDEP    theories/Numbers/Natural/Abstract/NBase.v
1204:info:build COQDEP    theories/Numbers/Natural/Abstract/NAxioms.v
1205:info:build COQDEP    theories/Numbers/Natural/Abstract/NAdd.v
1206:info:build COQDEP    theories/Numbers/Natural/Abstract/NAddOrder.v
1207:info:build COQDEP    theories/Numbers/NatInt/NZBits.v
1208:info:build COQDEP    theories/Numbers/NatInt/NZGcd.v
1209:info:build COQDEP    theories/Numbers/NatInt/NZLog.v
1210:info:build COQDEP    theories/Numbers/NatInt/NZSqrt.v
1211:info:build COQDEP    theories/Numbers/NatInt/NZPow.v
1212:info:build COQDEP    theories/Numbers/NatInt/NZDiv.v
1213:info:build COQDEP    theories/Numbers/NatInt/NZParity.v
1214:info:build COQDEP    theories/Numbers/NatInt/NZDomain.v
1215:info:build COQDEP    theories/Numbers/NatInt/NZProperties.v
1216:info:build COQDEP    theories/Numbers/NatInt/NZOrder.v
1217:info:build COQDEP    theories/Numbers/NatInt/NZMul.v
1218:info:build COQDEP    theories/Numbers/NatInt/NZMulOrder.v
1219:info:build COQDEP    theories/Numbers/NatInt/NZBase.v
1220:info:build COQDEP    theories/Numbers/NatInt/NZAxioms.v
1221:info:build COQDEP    theories/Numbers/NatInt/NZAdd.v
1222:info:build COQDEP    theories/Numbers/NatInt/NZAddOrder.v
1223:info:build COQDEP    theories/Numbers/NaryFunctions.v
1224:info:build COQDEP    theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v
1225:info:build COQDEP    theories/Numbers/Integer/SpecViaZ/ZSig.v
1226:info:build COQDEP    theories/Numbers/Integer/NatPairs/ZNatPairs.v
1227:info:build COQDEP    theories/Numbers/Integer/Binary/ZBinary.v
1228:info:build COQDEP    theories/Numbers/Integer/BigZ/ZMake.v
1229:info:build COQDEP    theories/Numbers/Integer/BigZ/BigZ.v
1230:info:build COQDEP    theories/Numbers/Integer/Abstract/ZProperties.v
1231:info:build COQDEP    theories/Numbers/Integer/Abstract/ZBits.v
1232:info:build COQDEP    theories/Numbers/Integer/Abstract/ZLcm.v
1233:info:build COQDEP    theories/Numbers/Integer/Abstract/ZGcd.v
1234:info:build COQDEP    theories/Numbers/Integer/Abstract/ZPow.v
1235:info:build COQDEP    theories/Numbers/Integer/Abstract/ZParity.v
1236:info:build COQDEP    theories/Numbers/Integer/Abstract/ZMaxMin.v
1237:info:build COQDEP    theories/Numbers/Integer/Abstract/ZDivEucl.v
1238:info:build COQDEP    theories/Numbers/Integer/Abstract/ZDivTrunc.v
1239:info:build COQDEP    theories/Numbers/Integer/Abstract/ZDivFloor.v
1240:info:build COQDEP    theories/Numbers/Integer/Abstract/ZSgnAbs.v
1241:info:build COQDEP    theories/Numbers/Integer/Abstract/ZMul.v
1242:info:build COQDEP    theories/Numbers/Integer/Abstract/ZMulOrder.v
1243:info:build COQDEP    theories/Numbers/Integer/Abstract/ZLt.v
1244:info:build COQDEP    theories/Numbers/Integer/Abstract/ZBase.v
1245:info:build COQDEP    theories/Numbers/Integer/Abstract/ZAxioms.v
1246:info:build COQDEP    theories/Numbers/Integer/Abstract/ZAdd.v
1247:info:build COQDEP    theories/Numbers/Integer/Abstract/ZAddOrder.v
1248:info:build COQDEP    theories/Numbers/Cyclic/ZModulo/ZModulo.v
1249:info:build COQDEP    theories/Numbers/Cyclic/Int31/Ring31.v
1250:info:build COQDEP    theories/Numbers/Cyclic/Int31/Cyclic31.v
1251:info:build COQDEP    theories/Numbers/Cyclic/Int31/Int31.v
1252:info:build COQDEP    theories/Numbers/Cyclic/DoubleCyclic/DoubleType.v
1253:info:build COQDEP    theories/Numbers/Cyclic/DoubleCyclic/DoubleSub.v
1254:info:build COQDEP    theories/Numbers/Cyclic/DoubleCyclic/DoubleSqrt.v
1255:info:build COQDEP    theories/Numbers/Cyclic/DoubleCyclic/DoubleMul.v
1256:info:build COQDEP    theories/Numbers/Cyclic/DoubleCyclic/DoubleLift.v
1257:info:build COQDEP    theories/Numbers/Cyclic/DoubleCyclic/DoubleDiv.v
1258:info:build COQDEP    theories/Numbers/Cyclic/DoubleCyclic/DoubleDivn1.v
1259:info:build COQDEP    theories/Numbers/Cyclic/DoubleCyclic/DoubleCyclic.v
1260:info:build COQDEP    theories/Numbers/Cyclic/DoubleCyclic/DoubleBase.v
1261:info:build COQDEP    theories/Numbers/Cyclic/DoubleCyclic/DoubleAdd.v
1262:info:build COQDEP    theories/Numbers/Cyclic/Abstract/NZCyclic.v
1263:info:build COQDEP    theories/Numbers/Cyclic/Abstract/CyclicAxioms.v
1264:info:build COQDEP    theories/Numbers/BigNumPrelude.v
1265:info:build COQDEP    theories/Numbers/BinNums.v
1266:info:build COQDEP    theories/QArith/Qminmax.v
1267:info:build COQDEP    theories/QArith/QOrderedType.v
1268:info:build COQDEP    theories/QArith/Qround.v
1269:info:build COQDEP    theories/QArith/Qring.v
1270:info:build COQDEP    theories/QArith/Qreduction.v
1271:info:build COQDEP    theories/QArith/Qreals.v
1272:info:build COQDEP    theories/QArith/Qpower.v
1273:info:build COQDEP    theories/QArith/Qfield.v
1274:info:build COQDEP    theories/QArith/Qcanon.v
1275:info:build COQDEP    theories/QArith/QArith.v
1276:info:build COQDEP    theories/QArith/QArith_base.v
1277:info:build COQDEP    theories/QArith/Qabs.v
1278:info:build COQDEP    theories/Sorting/Mergesort.v
1279:info:build COQDEP    theories/Sorting/Sorting.v
1280:info:build COQDEP    theories/Sorting/Sorted.v
1281:info:build COQDEP    theories/Sorting/PermutEq.v
1282:info:build COQDEP    theories/Sorting/PermutSetoid.v
1283:info:build COQDEP    theories/Sorting/Permutation.v
1284:info:build COQDEP    theories/Sorting/Heap.v
1285:info:build COQDEP    theories/Reals/Rminmax.v
1286:info:build COQDEP    theories/Reals/ROrderedType.v
1287:info:build COQDEP    theories/Reals/Sqrt_reg.v
1288:info:build COQDEP    theories/Reals/SplitRmult.v
1289:info:build COQDEP    theories/Reals/SplitAbsolu.v
1290:info:build COQDEP    theories/Reals/SeqSeries.v
1291:info:build COQDEP    theories/Reals/SeqProp.v
1292:info:build COQDEP    theories/Reals/Rtrigo.v
1293:info:build COQDEP    theories/Reals/Rtrigo1.v
1294:info:build COQDEP    theories/Reals/Rtrigo_reg.v
1295:info:build COQDEP    theories/Reals/Rtrigo_fun.v
1296:info:build COQDEP    theories/Reals/Rtrigo_def.v
1297:info:build COQDEP    theories/Reals/Rtrigo_calc.v
1298:info:build COQDEP    theories/Reals/Rtrigo_alt.v
1299:info:build COQDEP    theories/Reals/Rtopology.v
1300:info:build COQDEP    theories/Reals/R_sqr.v
1301:info:build COQDEP    theories/Reals/R_sqrt.v
1302:info:build COQDEP    theories/Reals/Rsqrt_def.v
1303:info:build COQDEP    theories/Reals/Rsigma.v
1304:info:build COQDEP    theories/Reals/Rseries.v
1305:info:build COQDEP    theories/Reals/Rprod.v
1306:info:build COQDEP    theories/Reals/Rpower.v
1307:info:build COQDEP    theories/Reals/Rpow_def.v
1308:info:build COQDEP    theories/Reals/Rlogic.v
1309:info:build COQDEP    theories/Reals/RList.v
1310:info:build COQDEP    theories/Reals/Rlimit.v
1311:info:build COQDEP    theories/Reals/RIneq.v
1312:info:build COQDEP    theories/Reals/R_Ifp.v
1313:info:build COQDEP    theories/Reals/RiemannInt.v
1314:info:build COQDEP    theories/Reals/RiemannInt_SF.v
1315:info:build COQDEP    theories/Reals/Rgeom.v
1316:info:build COQDEP    theories/Reals/Rfunctions.v
1317:info:build COQDEP    theories/Reals/Reals.v
1318:info:build COQDEP    theories/Reals/Rderiv.v
1319:info:build COQDEP    theories/Reals/Rdefinitions.v
1320:info:build COQDEP    theories/Reals/Rcomplete.v
1321:info:build COQDEP    theories/Reals/Rbasic_fun.v
1322:info:build COQDEP    theories/Reals/Rbase.v
1323:info:build COQDEP    theories/Reals/Raxioms.v
1324:info:build COQDEP    theories/Reals/Ratan.v
1325:info:build COQDEP    theories/Reals/Ranalysis_reg.v
1326:info:build COQDEP    theories/Reals/Ranalysis.v
1327:info:build COQDEP    theories/Reals/Ranalysis5.v
1328:info:build COQDEP    theories/Reals/Ranalysis4.v
1329:info:build COQDEP    theories/Reals/Ranalysis3.v
1330:info:build COQDEP    theories/Reals/Ranalysis2.v
1331:info:build COQDEP    theories/Reals/Ranalysis1.v
1332:info:build COQDEP    theories/Reals/PSeries_reg.v
1333:info:build COQDEP    theories/Reals/PartSum.v
1334:info:build COQDEP    theories/Reals/NewtonInt.v
1335:info:build COQDEP    theories/Reals/MVT.v
1336:info:build COQDEP    theories/Reals/Machin.v
1337:info:build COQDEP    theories/Reals/LegacyRfield.v
1338:info:build COQDEP    theories/Reals/Integration.v
1339:info:build COQDEP    theories/Reals/Exp_prop.v
1340:info:build COQDEP    theories/Reals/DiscrR.v
1341:info:build COQDEP    theories/Reals/Cos_rel.v
1342:info:build COQDEP    theories/Reals/Cos_plus.v
1343:info:build COQDEP    theories/Reals/Cauchy_prod.v
1344:info:build COQDEP    theories/Reals/Binomial.v
1345:info:build COQDEP    theories/Reals/ArithProp.v
1346:info:build COQDEP    theories/Reals/AltSeries.v
1347:info:build COQDEP    theories/Reals/Alembert.v
1348:info:build COQDEP    theories/Wellfounded/Well_Ordering.v
1349:info:build COQDEP    theories/Wellfounded/Wellfounded.v
1350:info:build COQDEP    theories/Wellfounded/Union.v
1351:info:build COQDEP    theories/Wellfounded/Transitive_Closure.v
1352:info:build COQDEP    theories/Wellfounded/Lexicographic_Product.v
1353:info:build COQDEP    theories/Wellfounded/Lexicographic_Exponentiation.v
1354:info:build COQDEP    theories/Wellfounded/Inverse_Image.v
1355:info:build COQDEP    theories/Wellfounded/Inclusion.v
1356:info:build COQDEP    theories/Wellfounded/Disjoint_Union.v
1357:info:build COQDEP    theories/Relations/Relations.v
1358:info:build COQDEP    theories/Relations/Relation_Operators.v
1359:info:build COQDEP    theories/Relations/Relation_Definitions.v
1360:info:build COQDEP    theories/Relations/Operators_Properties.v
1361:info:build COQDEP    theories/MSets/MSetPositive.v
1362:info:build COQDEP    theories/MSets/MSetWeakList.v
1363:info:build COQDEP    theories/MSets/MSetToFiniteSet.v
1364:info:build COQDEP    theories/MSets/MSets.v
1365:info:build COQDEP    theories/MSets/MSetProperties.v
1366:info:build COQDEP    theories/MSets/MSetList.v
1367:info:build COQDEP    theories/MSets/MSetInterface.v
1368:info:build COQDEP    theories/MSets/MSetFacts.v
1369:info:build COQDEP    theories/MSets/MSetEqProperties.v
1370:info:build COQDEP    theories/MSets/MSetDecide.v
1371:info:build COQDEP    theories/MSets/MSetRBT.v
1372:info:build COQDEP    theories/MSets/MSetAVL.v
1373:info:build COQDEP    theories/MSets/MSetGenTree.v
1374:info:build COQDEP    theories/FSets/FSetWeakList.v
1375:info:build COQDEP    theories/FSets/FSetToFiniteSet.v
1376:info:build COQDEP    theories/FSets/FSets.v
1377:info:build COQDEP    theories/FSets/FSetProperties.v
1378:info:build COQDEP    theories/FSets/FSetList.v
1379:info:build COQDEP    theories/FSets/FSetInterface.v
1380:info:build COQDEP    theories/FSets/FSetFacts.v
1381:info:build COQDEP    theories/FSets/FSetEqProperties.v
1382:info:build COQDEP    theories/FSets/FSetDecide.v
1383:info:build COQDEP    theories/FSets/FSetBridge.v
1384:info:build COQDEP    theories/FSets/FSetPositive.v
1385:info:build COQDEP    theories/FSets/FSetAVL.v
1386:info:build COQDEP    theories/FSets/FSetCompat.v
1387:info:build COQDEP    theories/FSets/FMapWeakList.v
1388:info:build COQDEP    theories/FSets/FMaps.v
1389:info:build COQDEP    theories/FSets/FMapPositive.v
1390:info:build COQDEP    theories/FSets/FMapList.v
1391:info:build COQDEP    theories/FSets/FMapInterface.v
1392:info:build COQDEP    theories/FSets/FMapFullAVL.v
1393:info:build COQDEP    theories/FSets/FMapFacts.v
1394:info:build COQDEP    theories/FSets/FMapAVL.v
1395:info:build COQDEP    theories/Sets/Uniset.v
1396:info:build COQDEP    theories/Sets/Relations_3.v
1397:info:build COQDEP    theories/Sets/Relations_3_facts.v
1398:info:build COQDEP    theories/Sets/Relations_2.v
1399:info:build COQDEP    theories/Sets/Relations_2_facts.v
1400:info:build COQDEP    theories/Sets/Relations_1.v
1401:info:build COQDEP    theories/Sets/Relations_1_facts.v
1402:info:build COQDEP    theories/Sets/Powerset.v
1403:info:build COQDEP    theories/Sets/Powerset_facts.v
1404:info:build COQDEP    theories/Sets/Powerset_Classical_facts.v
1405:info:build COQDEP    theories/Sets/Permut.v
1406:info:build COQDEP    theories/Sets/Partial_Order.v
1407:info:build COQDEP    theories/Sets/Multiset.v
1408:info:build COQDEP    theories/Sets/Integers.v
1409:info:build COQDEP    theories/Sets/Infinite_sets.v
1410:info:build COQDEP    theories/Sets/Image.v
1411:info:build COQDEP    theories/Sets/Finite_sets.v
1412:info:build COQDEP    theories/Sets/Finite_sets_facts.v
1413:info:build COQDEP    theories/Sets/Ensembles.v
1414:info:build COQDEP    theories/Sets/Cpo.v
1415:info:build COQDEP    theories/Sets/Constructive_sets.v
1416:info:build COQDEP    theories/Sets/Classical_sets.v
1417:info:build COQDEP    theories/Strings/String.v
1418:info:build COQDEP    theories/Strings/Ascii.v
1419:info:build COQDEP    theories/Lists/Streams.v
1420:info:build COQDEP    theories/Lists/StreamMemo.v
1421:info:build COQDEP    theories/Lists/SetoidPermutation.v
1422:info:build COQDEP    theories/Lists/SetoidList.v
1423:info:build COQDEP    theories/Lists/List.v
1424:info:build COQDEP    theories/Lists/ListTactics.v
1425:info:build COQDEP    theories/Lists/ListSet.v
1426:info:build COQDEP    theories/Setoids/Setoid.v
1427:info:build COQDEP    theories/ZArith/Zeuclid.v
1428:info:build COQDEP    theories/ZArith/Zwf.v
1429:info:build COQDEP    theories/ZArith/Zsqrt_compat.v
1430:info:build COQDEP    theories/ZArith/Zpow_facts.v
1431:info:build COQDEP    theories/ZArith/Zpower.v
1432:info:build COQDEP    theories/ZArith/Zpow_def.v
1433:info:build COQDEP    theories/ZArith/Zorder.v
1434:info:build COQDEP    theories/ZArith/Zquot.v
1435:info:build COQDEP    theories/ZArith/ZOdiv.v
1436:info:build COQDEP    theories/ZArith/ZOdiv_def.v
1437:info:build COQDEP    theories/ZArith/Znumtheory.v
1438:info:build COQDEP    theories/ZArith/Znat.v
1439:info:build COQDEP    theories/ZArith/Zmisc.v
1440:info:build COQDEP    theories/ZArith/Zmin.v
1441:info:build COQDEP    theories/ZArith/Zminmax.v
1442:info:build COQDEP    theories/ZArith/Zmax.v
1443:info:build COQDEP    theories/ZArith/Zlogarithm.v
1444:info:build COQDEP    theories/ZArith/Zhints.v
1445:info:build COQDEP    theories/ZArith/Zpow_alt.v
1446:info:build COQDEP    theories/ZArith/Zgcd_alt.v
1447:info:build COQDEP    theories/ZArith/Zeven.v
1448:info:build COQDEP    theories/ZArith/Zdiv.v
1449:info:build COQDEP    theories/ZArith/Zcomplements.v
1450:info:build COQDEP    theories/ZArith/Zcompare.v
1451:info:build COQDEP    theories/ZArith/Zbool.v
1452:info:build COQDEP    theories/ZArith/Zdigits.v
1453:info:build COQDEP    theories/ZArith/ZArith.v
1454:info:build COQDEP    theories/ZArith/ZArith_dec.v
1455:info:build COQDEP    theories/ZArith/ZArith_base.v
1456:info:build COQDEP    theories/ZArith/Zabs.v
1457:info:build COQDEP    theories/ZArith/Wf_Z.v
1458:info:build COQDEP    theories/ZArith/Int.v
1459:info:build COQDEP    theories/ZArith/BinInt.v
1460:info:build COQDEP    theories/ZArith/BinIntDef.v
1461:info:build COQDEP    theories/ZArith/auxiliary.v
1462:info:build COQDEP    theories/NArith/Ngcd_def.v
1463:info:build COQDEP    theories/NArith/Nsqrt_def.v
1464:info:build COQDEP    theories/NArith/Ndiv_def.v
1465:info:build COQDEP    theories/NArith/Nnat.v
1466:info:build COQDEP    theories/NArith/Ndist.v
1467:info:build COQDEP    theories/NArith/Ndigits.v
1468:info:build COQDEP    theories/NArith/Ndec.v
1469:info:build COQDEP    theories/NArith/NArith.v
1470:info:build COQDEP    theories/NArith/BinNat.v
1471:info:build COQDEP    theories/NArith/BinNatDef.v
1472:info:build COQDEP    theories/PArith/PArith.v
1473:info:build COQDEP    theories/PArith/POrderedType.v
1474:info:build COQDEP    theories/PArith/Pnat.v
1475:info:build COQDEP    theories/PArith/BinPos.v
1476:info:build COQDEP    theories/PArith/BinPosDef.v
1477:info:build COQDEP    theories/Bool/Zerob.v
1478:info:build COQDEP    theories/Bool/Sumbool.v
1479:info:build COQDEP    theories/Bool/IfProp.v
1480:info:build COQDEP    theories/Bool/DecBool.v
1481:info:build COQDEP    theories/Bool/Bvector.v
1482:info:build COQDEP    theories/Bool/Bool.v
1483:info:build COQDEP    theories/Bool/BoolEq.v
1484:info:build COQDEP    theories/Arith/Wf_nat.v
1485:info:build COQDEP    theories/Arith/Plus.v
1486:info:build COQDEP    theories/Arith/Peano_dec.v
1487:info:build COQDEP    theories/Arith/Mult.v
1488:info:build COQDEP    theories/Arith/Min.v
1489:info:build COQDEP    theories/Arith/Minus.v
1490:info:build COQDEP    theories/Arith/Max.v
1491:info:build COQDEP    theories/Arith/Lt.v
1492:info:build COQDEP    theories/Arith/Le.v
1493:info:build COQDEP    theories/Arith/Gt.v
1494:info:build COQDEP    theories/Arith/Factorial.v
1495:info:build COQDEP    theories/Arith/Euclid.v
1496:info:build COQDEP    theories/Arith/Even.v
1497:info:build COQDEP    theories/Arith/EqNat.v
1498:info:build COQDEP    theories/Arith/Div2.v
1499:info:build COQDEP    theories/Arith/Compare.v
1500:info:build COQDEP    theories/Arith/Compare_dec.v
1501:info:build COQDEP    theories/Arith/Bool_nat.v
1502:info:build COQDEP    theories/Arith/Between.v
1503:info:build COQDEP    theories/Arith/Arith.v
1504:info:build COQDEP    theories/Arith/Arith_base.v
1505:info:build COQDEP    theories/Logic/SetIsType.v
1506:info:build COQDEP    theories/Logic/RelationalChoice.v
1507:info:build COQDEP    theories/Logic/ProofIrrelevance.v
1508:info:build COQDEP    theories/Logic/ProofIrrelevanceFacts.v
1509:info:build COQDEP    theories/Logic/JMeq.v
1510:info:build COQDEP    theories/Logic/IndefiniteDescription.v
1511:info:build COQDEP    theories/Logic/Hurkens.v
1512:info:build COQDEP    theories/Logic/ExtensionalityFacts.v
1513:info:build COQDEP    theories/Logic/FunctionalExtensionality.v
1514:info:build COQDEP    theories/Logic/Eqdep.v
1515:info:build COQDEP    theories/Logic/EqdepFacts.v
1516:info:build COQDEP    theories/Logic/Eqdep_dec.v
1517:info:build COQDEP    theories/Logic/Epsilon.v
1518:info:build COQDEP    theories/Logic/Diaconescu.v
1519:info:build COQDEP    theories/Logic/Description.v
1520:info:build COQDEP    theories/Logic/Decidable.v
1521:info:build COQDEP    theories/Logic/ConstructiveEpsilon.v
1522:info:build COQDEP    theories/Logic/Classical.v
1523:info:build COQDEP    theories/Logic/ClassicalUniqueChoice.v
1524:info:build COQDEP    theories/Logic/Classical_Type.v
1525:info:build COQDEP    theories/Logic/Classical_Prop.v
1526:info:build COQDEP    theories/Logic/Classical_Pred_Type.v
1527:info:build COQDEP    theories/Logic/Classical_Pred_Set.v
1528:info:build COQDEP    theories/Logic/ClassicalFacts.v
1529:info:build COQDEP    theories/Logic/ClassicalEpsilon.v
1530:info:build COQDEP    theories/Logic/ClassicalDescription.v
1531:info:build COQDEP    theories/Logic/ClassicalChoice.v
1532:info:build COQDEP    theories/Logic/ChoiceFacts.v
1533:info:build COQDEP    theories/Logic/Berardi.v
1534:info:build COQDEP    theories/Init/Wf.v
1535:info:build COQDEP    theories/Init/Tactics.v
1536:info:build COQDEP    theories/Init/Specif.v
1537:info:build COQDEP    theories/Init/Prelude.v
1538:info:build COQDEP    theories/Init/Peano.v
1539:info:build COQDEP    theories/Init/Notations.v
1540:info:build COQDEP    theories/Init/Logic.v
1541:info:build COQDEP    theories/Init/Logic_Type.v
1542:info:build COQDEP    theories/Init/Datatypes.v
1543:info:build COQDEP  toplevel/toplevel.mllib
1544:info:build COQDEP  tools/win32hack.mllib
1545:info:build COQDEP  tactics/tactics.mllib
1546:info:build COQDEP  tactics/hightactics.mllib
1547:info:build COQDEP  proofs/proofs.mllib
1548:info:build COQDEP  pretyping/pretyping.mllib
1549:info:build COQDEP  plugins/xml/xml_plugin.mllib
1550:info:build COQDEP  plugins/syntax/z_syntax_plugin.mllib
1551:info:build COQDEP  plugins/syntax/string_syntax_plugin.mllib
1552:info:build COQDEP  plugins/syntax/r_syntax_plugin.mllib
1553:info:build COQDEP  plugins/syntax/numbers_syntax_plugin.mllib
1554:info:build COQDEP  plugins/syntax/nat_syntax_plugin.mllib
1555:info:build COQDEP  plugins/syntax/ascii_syntax_plugin.mllib
1556:info:build COQDEP  plugins/subtac/subtac_plugin.mllib
1557:info:build COQDEP  plugins/setoid_ring/newring_plugin.mllib
1558:info:build COQDEP  plugins/rtauto/rtauto_plugin.mllib
1559:info:build COQDEP  plugins/romega/romega_plugin.mllib
1560:info:build COQDEP  plugins/ring/ring_plugin.mllib
1561:info:build COQDEP  plugins/quote/quote_plugin.mllib
1562:info:build COQDEP  plugins/omega/omega_plugin.mllib
1563:info:build COQDEP  plugins/nsatz/nsatz_plugin.mllib
1564:info:build COQDEP  plugins/micromega/micromega_plugin.mllib
1565:info:build COQDEP  plugins/funind/recdef_plugin.mllib
1566:info:build COQDEP  plugins/fourier/fourier_plugin.mllib
1567:info:build COQDEP  plugins/firstorder/ground_plugin.mllib
1568:info:build COQDEP  plugins/field/field_plugin.mllib
1569:info:build COQDEP  plugins/extraction/extraction_plugin.mllib
1570:info:build COQDEP  plugins/decl_mode/decl_mode_plugin.mllib
1571:info:build COQDEP  plugins/cc/cc_plugin.mllib
1572:info:build COQDEP  parsing/parsing.mllib
1573:info:build COQDEP  parsing/highparsing.mllib
1574:info:build COQDEP  parsing/grammar.mllib
1575:info:build COQDEP  library/library.mllib
1576:info:build COQDEP  lib/lib.mllib
1577:info:build COQDEP  kernel/kernel.mllib
1578:info:build COQDEP  interp/interp.mllib
1579:info:build COQDEP  ide/ide.mllib
1580:info:build COQDEP  dev/printers.mllib
1581:info:build COQDEP  checker/check.mllib
1582:info:build make[1]: Leaving directory `/opt/local/var/macports/build/_opt_local_var_macports_sources_rsync.macports.org_release_tarballs_ports_lang_coq/coq/work/coq-8.4pl6'
1583:info:build make[1]: Entering directory `/opt/local/var/macports/build/_opt_local_var_macports_sources_rsync.macports.org_release_tarballs_ports_lang_coq/coq/work/coq-8.4pl6'
1584:info:build OCAMLC    config/coq_config.mli
1585:info:build OCAMLC    lib/profile.mli
1586:info:build OCAMLC    lib/pp_control.mli
1587:info:build CAMLP4O   lib/pp.ml4
1588:info:build CAMLP4O   lib/compat.ml4
1589:info:build OCAMLC    lib/flags.mli
1590:info:build OCAMLC    lib/segmenttree.mli
1591:info:build Error while loading "tools/compat5.cmo": interface mismatch on CamlinternalFormatBasics.
1592:info:build make[1]: *** [lib/pp.ml] Error 2
1593:info:build make[1]: *** Waiting for unfinished jobs....
1594:info:build Error while loading "tools/compat5.cmo": interface mismatch on CamlinternalFormatBasics.
1595:info:build make[1]: *** [lib/compat.ml] Error 2
1596:info:build make[1]: Leaving directory `/opt/local/var/macports/build/_opt_local_var_macports_sources_rsync.macports.org_release_tarballs_ports_lang_coq/coq/work/coq-8.4pl6'
1597:info:build make: *** [world] Error 2
1598:info:build make: Leaving directory `/opt/local/var/macports/build/_opt_local_var_macports_sources_rsync.macports.org_release_tarballs_ports_lang_coq/coq/work/coq-8.4pl6'
1599:info:build Command failed:  cd "/opt/local/var/macports/build/_opt_local_var_macports_sources_rsync.macports.org_release_tarballs_ports_lang_coq/coq/work/coq-8.4pl6" && /usr/bin/make -j4 -w world
1600:info:build Exit code: 2
1601:error:build org.macports.build for port coq returned: command execution failed
1602:debug:build Error code: CHILDSTATUS 53916 2
1603:debug:build Backtrace: command execution failed
1604    while executing
1605"system -nice 0 $fullcmdstring"
1606    ("eval" body line 1)
1607    invoked from within
1608"eval system $notty $nice \$fullcmdstring"
1609    invoked from within
1610"command_exec build"
1611    (procedure "portbuild::build_main" line 8)
1612    invoked from within
1613"portbuild::build_main org.macports.build"
1614    ("eval" body line 1)
1615    invoked from within
1616"eval $procedure $targetname"
1617:info:build Warning: targets not executed for coq: org.macports.activate org.macports.build org.macports.destroot org.macports.install
1618:notice:build Please see the log file for port coq for details:
1619    /opt/local/var/macports/logs/_opt_local_var_macports_sources_rsync.macports.org_release_tarballs_ports_lang_coq/coq/main.log