Go to:
Gentoo Home
Documentation
Forums
Lists
Bugs
Planet
Store
Wiki
Get Gentoo!
Gentoo's Bugzilla – Attachment 209799 Details for
Bug 292630
Problem emerging sci-mathematics/coq-8.2_p1-r1
Home
|
New
–
[Ex]
|
Browse
|
Search
|
Privacy Policy
|
[?]
|
Reports
|
Requests
|
Help
|
New Account
|
Log In
[x]
|
Forgot Password
Login:
[x]
Build log file
build.log (text/plain), 157.33 KB, created by
Pierre
on 2009-11-10 02:30:11 UTC
(
hide
)
Description:
Build log file
Filename:
MIME Type:
Creator:
Pierre
Created:
2009-11-10 02:30:11 UTC
Size:
157.33 KB
patch
obsolete
>>>> Unpacking source... >>>> Unpacking coq-8.2pl1.tar.gz to /var/tmp/portage/sci-mathematics/coq-8.2_p1-r1/work >>>> Source unpacked in /var/tmp/portage/sci-mathematics/coq-8.2_p1-r1/work >>>> Preparing source in /var/tmp/portage/sci-mathematics/coq-8.2_p1-r1/work/coq-8.2pl1 ... >>>> Source prepared. >>>> Configuring source in /var/tmp/portage/sci-mathematics/coq-8.2_p1-r1/work/coq-8.2pl1 ... >You have GNU Make 3.81. Good! >You have Objective-Caml 3.10.2. Good! >You have native-code compilation. Good! >LablGtk2 found, native threads: native CoqIde will be available. > > Coq top directory : /var/tmp/portage/sci-mathematics/coq-8.2_p1-r1/work/coq-8.2pl1 > Architecture : x86_64 > Coq VM bytecode link flags : -dllib -lcoqrun -dllpath '/usr/lib64/coq' > Coq tools bytecode link flags : > OS dependent libraries : -cclib -lunix > Objective-Caml/Camlp4 version : 3.10.2 > Objective-Caml/Camlp4 binaries in : /usr/bin > Objective-Caml library in : /usr/lib64/ocaml > Camlp4 library in : /usr/lib64/ocaml/camlp5 > Lablgtk2 library in : /usr/lib64/ocaml/lablgtk2 > FSets theory : All > Reals theory : All > Documentation : All > CoqIde : opt > Web browser : firefox -remote "OpenURL(%s,new-tab)" || firefox %s & > Coq web site : http://www.lix.polytechnique.fr/coq/ > > Paths for true installation: > binaries will be copied in /usr/bin > library will be copied in /usr/lib64/coq > man pages will be copied in /usr/share/man > documentation will be copied in /usr/share/doc/coq-8.2_p1-r1 > emacs mode will be copied in /usr/share/emacs/site-lisp > >If anything in the above is wrong, please restart './configure' > >*Warning* To compile the system for a new architecture > don't forget to do a 'make archclean' before './configure'. >>>> Source configured. >>>> Compiling source in /var/tmp/portage/sci-mathematics/coq-8.2_p1-r1/work/coq-8.2pl1 ... >make STRIP=true -j1 >***************************************************** >***************************************************** >****************** Entering stage1 ****************** >***************************************************** >***************************************************** >make -f Makefile.stage1 "stage1" >make[1]: Entering directory `/var/tmp/portage/sci-mathematics/coq-8.2_p1-r1/work/coq-8.2pl1' >sed -n -e '/^ /s/ \([A-Z]\)/ \&\&coq_lbl_\1/gp' \ > -e '/^}/q' kernel/byterun/coq_instruct.h > \ > kernel/byterun/coq_jumptbl.h \ > || ( RV=$?; rm -f "kernel/byterun/coq_jumptbl.h"; exit ${RV} ) >CCDEP kernel/byterun/coq_memory.c >CCDEP kernel/byterun/coq_values.c >CCDEP kernel/byterun/coq_interp.c >CCDEP kernel/byterun/coq_fix_code.c >OCAMLLEX dev/ocamlweb-doc/lex.mll >99 states, 6415 transitions, table size 26254 bytes >OCAMLLEX tools/coqdoc/index.mll >218 states, 5403 transitions, table size 22920 bytes >OCAMLLEX tools/coqdoc/pretty.mll >2084 states, 19449 transitions, table size 90300 bytes >OCAMLLEX tools/coqwc.mll >183 states, 833 transitions, table size 4430 bytes >OCAMLLEX tools/coqdep_lexer.mll >181 states, 5332 transitions, table size 22414 bytes >OCAMLLEX tools/gallina_lexer.mll >151 states, 498 transitions, table size 2898 bytes >OCAMLLEX contrib/dp/dp_zenon.mll >77 states, 637 transitions, table size 3010 bytes >1833 additional bytes used for bindings >OCAMLLEX ide/utf8_convert.mll >15 states, 827 transitions, table size 3398 bytes >OCAMLLEX ide/extract_index.mll >29 states, 269 transitions, table size 1250 bytes >OCAMLLEX ide/find_phrase.mll >15 states, 265 transitions, table size 1150 bytes >OCAMLLEX ide/highlight.mll >310 states, 28058 transitions, table size 114092 bytes >OCAMLLEX ide/config_lexer.mll >13 states, 332 transitions, table size 1406 bytes >OCAMLYACC dev/ocamlweb-doc/syntax.mly >3 shift/reduce conflicts. >OCAMLYACC ide/config_parser.mly >ECHO... > scripts/tolink.ml >sed -n -e '/^enum/p' -e 's/,//g' -e '/^ /p' \ > kernel/byterun/coq_instruct.h | \ > awk -f kernel/make-opcodes > kernel/copcodes.ml \ > || ( RV=$?; rm -f "kernel/copcodes.ml"; exit ${RV} ) >"ocaml" theories/Numbers/Natural/BigN/NMake_gen.ml > theories/Numbers/Natural/BigN/NMake.v >TOUCH lib/pp.ml >TOUCH lib/compat.ml >TOUCH toplevel/mltop.ml >TOUCH toplevel/whelp.ml >TOUCH tactics/hipattern.ml >TOUCH tactics/eqdecide.ml >TOUCH tactics/tauto.ml >TOUCH tactics/extratactics.ml >TOUCH tactics/class_tactics.ml >TOUCH tactics/eauto.ml >TOUCH tactics/extraargs.ml >TOUCH tools/coq-tex.ml >TOUCH tools/coq_makefile.ml >TOUCH contrib/setoid_ring/newring.ml >TOUCH contrib/ring/g_quote.ml >TOUCH contrib/ring/g_ring.ml >TOUCH contrib/rtauto/g_rtauto.ml >TOUCH contrib/interface/debug_tac.ml >TOUCH contrib/interface/line_parser.ml >TOUCH contrib/interface/centaur.ml >TOUCH contrib/field/field.ml >TOUCH contrib/cc/g_congruence.ml >TOUCH contrib/extraction/g_extraction.ml >TOUCH contrib/romega/g_romega.ml >TOUCH contrib/fourier/g_fourier.ml >TOUCH contrib/subtac/equations.ml >TOUCH contrib/subtac/g_eterm.ml >TOUCH contrib/subtac/g_subtac.ml >TOUCH contrib/xml/proofTree2Xml.ml >TOUCH contrib/xml/dumptree.ml >TOUCH contrib/xml/xml.ml >TOUCH contrib/xml/xmlentries.ml >TOUCH contrib/xml/acic2Xml.ml >TOUCH contrib/funind/g_indfun.ml >TOUCH contrib/firstorder/g_ground.ml >TOUCH contrib/omega/g_omega.ml >TOUCH contrib/micromega/g_micromega.ml >TOUCH contrib/dp/g_dp.ml >TOUCH parsing/g_proofs.ml >TOUCH parsing/g_ltac.ml >TOUCH parsing/g_tactic.ml >TOUCH parsing/q_coqast.ml >TOUCH parsing/g_constr.ml >TOUCH parsing/argextend.ml >TOUCH parsing/g_xml.ml >TOUCH parsing/q_util.ml >TOUCH parsing/g_vernac.ml >TOUCH parsing/tacextend.ml >TOUCH parsing/q_constr.ml >TOUCH parsing/lexer.ml >TOUCH parsing/pcoq.ml >TOUCH parsing/g_prim.ml >TOUCH parsing/vernacextend.ml >TOUCH parsing/g_decl_mode.ml >CAMLP4DEPS parsing/q_constr.ml4 >OCAMLDEP4 parsing/q_constr.ml4 >CAMLP4DEPS parsing/q_coqast.ml4 >OCAMLDEP4 parsing/q_coqast.ml4 >CAMLP4DEPS parsing/lexer.ml4 >OCAMLDEP4 parsing/lexer.ml4 >CAMLP4DEPS parsing/g_constr.ml4 >OCAMLDEP4 parsing/g_constr.ml4 >CAMLP4DEPS parsing/g_ltac.ml4 >OCAMLDEP4 parsing/g_ltac.ml4 >CAMLP4DEPS parsing/g_tactic.ml4 >OCAMLDEP4 parsing/g_tactic.ml4 >CAMLP4DEPS parsing/g_prim.ml4 >OCAMLDEP4 parsing/g_prim.ml4 >CAMLP4DEPS parsing/vernacextend.ml4 >OCAMLDEP4 parsing/vernacextend.ml4 >CAMLP4DEPS parsing/tacextend.ml4 >OCAMLDEP4 parsing/tacextend.ml4 >CAMLP4DEPS parsing/argextend.ml4 >OCAMLDEP4 parsing/argextend.ml4 >CAMLP4DEPS parsing/pcoq.ml4 >OCAMLDEP4 parsing/pcoq.ml4 >CAMLP4DEPS parsing/q_util.ml4 >OCAMLDEP4 parsing/q_util.ml4 >CAMLP4DEPS lib/pp.ml4 >OCAMLDEP4 lib/pp.ml4 >CAMLP4DEPS lib/compat.ml4 >OCAMLDEP4 lib/compat.ml4 >OCAMLDEP ide/config_parser.mli >OCAMLDEP dev/ocamlweb-doc/syntax.mli >OCAMLDEP ide/utils/okey.mli >OCAMLDEP ide/utils/uoptions.mli >OCAMLDEP ide/utils/configwin.mli >OCAMLDEP ide/utils/config_file.mli >OCAMLDEP ide/undo_lablgtk_ge26.mli >OCAMLDEP ide/coqide.mli >OCAMLDEP ide/preferences.mli >OCAMLDEP ide/undo.mli >OCAMLDEP ide/command_windows.mli >OCAMLDEP ide/undo_lablgtk_lt26.mli >OCAMLDEP ide/undo_lablgtk_ge212.mli >OCAMLDEP ide/coq_tactics.mli >OCAMLDEP ide/ideutils.mli >OCAMLDEP ide/coq.mli >OCAMLDEP checker/declarations.mli >OCAMLDEP checker/subtyping.mli >OCAMLDEP checker/check_stat.mli >OCAMLDEP checker/indtypes.mli >OCAMLDEP checker/reduction.mli >OCAMLDEP checker/typeops.mli >OCAMLDEP checker/safe_typing.mli >OCAMLDEP checker/closure.mli >OCAMLDEP checker/environ.mli >OCAMLDEP checker/modops.mli >OCAMLDEP checker/term.mli >OCAMLDEP checker/inductive.mli >OCAMLDEP checker/type_errors.mli >OCAMLDEP parsing/lexer.mli >OCAMLDEP parsing/tactic_printer.mli >OCAMLDEP parsing/egrammar.mli >OCAMLDEP parsing/ppdecl_proof.mli >OCAMLDEP parsing/printmod.mli >OCAMLDEP parsing/g_minicoq.mli >OCAMLDEP parsing/q_util.mli >OCAMLDEP parsing/printer.mli >OCAMLDEP parsing/prettyp.mli >OCAMLDEP parsing/search.mli >OCAMLDEP parsing/extend.mli >OCAMLDEP parsing/pcoq.mli >OCAMLDEP parsing/ppvernac.mli >OCAMLDEP parsing/ppconstr.mli >OCAMLDEP parsing/g_intsyntax.mli >OCAMLDEP parsing/g_zsyntax.mli >OCAMLDEP parsing/g_natsyntax.mli >OCAMLDEP parsing/pptactic.mli >OCAMLDEP interp/implicit_quantifiers.mli >OCAMLDEP interp/topconstr.mli >OCAMLDEP interp/constrintern.mli >OCAMLDEP interp/reserve.mli >OCAMLDEP interp/constrextern.mli >OCAMLDEP interp/modintern.mli >OCAMLDEP interp/syntax_def.mli >OCAMLDEP interp/notation.mli >OCAMLDEP interp/ppextend.mli >OCAMLDEP interp/dumpglob.mli >OCAMLDEP interp/coqlib.mli >OCAMLDEP interp/genarg.mli >OCAMLDEP contrib/dp/dp_zenon.mli >OCAMLDEP contrib/dp/dp_why.mli >OCAMLDEP contrib/dp/fol.mli >OCAMLDEP contrib/dp/dp.mli >OCAMLDEP contrib/micromega/micromega.mli >OCAMLDEP contrib/micromega/sos.mli >OCAMLDEP contrib/firstorder/sequent.mli >OCAMLDEP contrib/firstorder/unify.mli >OCAMLDEP contrib/firstorder/instances.mli >OCAMLDEP contrib/firstorder/ground.mli >OCAMLDEP contrib/firstorder/formula.mli >OCAMLDEP contrib/firstorder/rules.mli >OCAMLDEP contrib/funind/functional_principles_proofs.mli >OCAMLDEP contrib/funind/indfun_common.mli >OCAMLDEP contrib/funind/functional_principles_types.mli >OCAMLDEP contrib/funind/rawterm_to_relation.mli >OCAMLDEP contrib/funind/rawtermops.mli >OCAMLDEP contrib/xml/xmlcommand.mli >OCAMLDEP contrib/xml/xml.mli >OCAMLDEP contrib/xml/doubleTypeInference.mli >OCAMLDEP contrib/xml/unshare.mli >OCAMLDEP contrib/subtac/subtac_cases.mli >OCAMLDEP contrib/subtac/eterm.mli >OCAMLDEP contrib/subtac/subtac_pretyping.mli >OCAMLDEP contrib/subtac/subtac_obligations.mli >OCAMLDEP contrib/subtac/subtac_utils.mli >OCAMLDEP contrib/subtac/subtac_command.mli >OCAMLDEP contrib/subtac/subtac_errors.mli >OCAMLDEP contrib/subtac/subtac_coercion.mli >OCAMLDEP contrib/subtac/subtac_classes.mli >OCAMLDEP contrib/subtac/subtac.mli >OCAMLDEP contrib/romega/const_omega.mli >OCAMLDEP contrib/extraction/extract_env.mli >OCAMLDEP contrib/extraction/table.mli >OCAMLDEP contrib/extraction/modutil.mli >OCAMLDEP contrib/extraction/miniml.mli >OCAMLDEP contrib/extraction/mlutil.mli >OCAMLDEP contrib/extraction/scheme.mli >OCAMLDEP contrib/extraction/extraction.mli >OCAMLDEP contrib/extraction/haskell.mli >OCAMLDEP contrib/extraction/common.mli >OCAMLDEP contrib/extraction/ocaml.mli >OCAMLDEP contrib/cc/ccproof.mli >OCAMLDEP contrib/cc/ccalgo.mli >OCAMLDEP contrib/cc/cctac.mli >OCAMLDEP contrib/interface/paths.mli >OCAMLDEP contrib/interface/debug_tac.mli >OCAMLDEP contrib/interface/name_to_ast.mli >OCAMLDEP contrib/interface/dad.mli >OCAMLDEP contrib/interface/blast.mli >OCAMLDEP contrib/interface/translate.mli >OCAMLDEP contrib/interface/showproof.mli >OCAMLDEP contrib/interface/pbp.mli >OCAMLDEP contrib/interface/vtp.mli >OCAMLDEP contrib/interface/xlate.mli >OCAMLDEP contrib/interface/ascent.mli >OCAMLDEP contrib/interface/history.mli >OCAMLDEP contrib/interface/line_parser.mli >OCAMLDEP contrib/rtauto/proof_search.mli >OCAMLDEP contrib/rtauto/refl_tauto.mli >OCAMLDEP tools/coqdoc/alpha.mli >OCAMLDEP tools/coqdoc/output.mli >OCAMLDEP tools/coqdoc/index.mli >OCAMLDEP tools/coqdoc/pretty.mli >OCAMLDEP library/summary.mli >OCAMLDEP library/states.mli >OCAMLDEP library/library.mli >OCAMLDEP library/nameops.mli >OCAMLDEP library/libnames.mli >OCAMLDEP library/declaremods.mli >OCAMLDEP library/heads.mli >OCAMLDEP library/decls.mli >OCAMLDEP library/impargs.mli >OCAMLDEP library/lib.mli >OCAMLDEP library/nametab.mli >OCAMLDEP library/goptions.mli >OCAMLDEP library/declare.mli >OCAMLDEP library/dischargedhypsmap.mli >OCAMLDEP library/global.mli >OCAMLDEP library/libobject.mli >OCAMLDEP library/decl_kinds.mli >OCAMLDEP proofs/evar_refiner.mli >OCAMLDEP proofs/tactic_debug.mli >OCAMLDEP proofs/refiner.mli >OCAMLDEP proofs/clenvtac.mli >OCAMLDEP proofs/logic.mli >OCAMLDEP proofs/decl_mode.mli >OCAMLDEP proofs/proof_type.mli >OCAMLDEP proofs/redexpr.mli >OCAMLDEP proofs/pfedit.mli >OCAMLDEP proofs/proof_trees.mli >OCAMLDEP proofs/decl_expr.mli >OCAMLDEP proofs/tacmach.mli >OCAMLDEP tactics/decl_interp.mli >OCAMLDEP tactics/hipattern.mli >OCAMLDEP tactics/tactics.mli >OCAMLDEP tactics/dn.mli >OCAMLDEP tactics/evar_tactics.mli >OCAMLDEP tactics/decl_proof_instr.mli >OCAMLDEP tactics/leminv.mli >OCAMLDEP tactics/elim.mli >OCAMLDEP tactics/equality.mli >OCAMLDEP tactics/hiddentac.mli >OCAMLDEP tactics/contradiction.mli >OCAMLDEP tactics/dhyp.mli >OCAMLDEP tactics/eauto.mli >OCAMLDEP tactics/extratactics.mli >OCAMLDEP tactics/extraargs.mli >OCAMLDEP tactics/inv.mli >OCAMLDEP tactics/termdn.mli >OCAMLDEP tactics/auto.mli >OCAMLDEP tactics/refine.mli >OCAMLDEP tactics/btermdn.mli >OCAMLDEP tactics/tacticals.mli >OCAMLDEP tactics/autorewrite.mli >OCAMLDEP tactics/tacinterp.mli >OCAMLDEP tactics/nbtermdn.mli >OCAMLDEP toplevel/auto_ind_decl.mli >OCAMLDEP toplevel/class.mli >OCAMLDEP toplevel/toplevel.mli >OCAMLDEP toplevel/metasyntax.mli >OCAMLDEP toplevel/ind_tables.mli >OCAMLDEP toplevel/vernacinterp.mli >OCAMLDEP toplevel/vernacentries.mli >OCAMLDEP toplevel/fhimsg.mli >OCAMLDEP toplevel/himsg.mli >OCAMLDEP toplevel/line_oriented_parser.mli >OCAMLDEP toplevel/whelp.mli >OCAMLDEP toplevel/coqtop.mli >OCAMLDEP toplevel/protectedtoplevel.mli >OCAMLDEP toplevel/mltop.mli >OCAMLDEP toplevel/discharge.mli >OCAMLDEP toplevel/coqinit.mli >OCAMLDEP toplevel/command.mli >OCAMLDEP toplevel/record.mli >OCAMLDEP toplevel/searchisos.mli >OCAMLDEP toplevel/classes.mli >OCAMLDEP toplevel/cerrors.mli >OCAMLDEP toplevel/usage.mli >OCAMLDEP toplevel/vernac.mli >OCAMLDEP lib/option.mli >OCAMLDEP lib/flags.mli >OCAMLDEP lib/predicate.mli >OCAMLDEP lib/hashcons.mli >OCAMLDEP lib/system.mli >OCAMLDEP lib/profile.mli >OCAMLDEP lib/envars.mli >OCAMLDEP lib/tlm.mli >OCAMLDEP lib/bigint.mli >OCAMLDEP lib/heap.mli >OCAMLDEP lib/pp_control.mli >OCAMLDEP lib/pp.mli >OCAMLDEP lib/util.mli >OCAMLDEP lib/rtree.mli >OCAMLDEP lib/edit.mli >OCAMLDEP lib/dyn.mli >OCAMLDEP lib/gmap.mli >OCAMLDEP lib/gset.mli >OCAMLDEP lib/explore.mli >OCAMLDEP lib/gmapl.mli >OCAMLDEP lib/bstack.mli >OCAMLDEP config/coq_config.mli >OCAMLDEP pretyping/inductiveops.mli >OCAMLDEP pretyping/evd.mli >OCAMLDEP pretyping/pretype_errors.mli >OCAMLDEP pretyping/pattern.mli >OCAMLDEP pretyping/indrec.mli >OCAMLDEP pretyping/matching.mli >OCAMLDEP pretyping/typeclasses_errors.mli >OCAMLDEP pretyping/tacred.mli >OCAMLDEP pretyping/vnorm.mli >OCAMLDEP pretyping/reductionops.mli >OCAMLDEP pretyping/recordops.mli >OCAMLDEP pretyping/cases.mli >OCAMLDEP pretyping/typeclasses.mli >OCAMLDEP pretyping/unification.mli >OCAMLDEP pretyping/evarutil.mli >OCAMLDEP pretyping/typing.mli >OCAMLDEP pretyping/cbv.mli >OCAMLDEP pretyping/termops.mli >OCAMLDEP pretyping/detyping.mli >OCAMLDEP pretyping/retyping.mli >OCAMLDEP pretyping/clenv.mli >OCAMLDEP pretyping/pretyping.mli >OCAMLDEP pretyping/coercion.mli >OCAMLDEP pretyping/classops.mli >OCAMLDEP pretyping/evarconv.mli >OCAMLDEP pretyping/rawterm.mli >OCAMLDEP kernel/esubst.mli >OCAMLDEP kernel/declarations.mli >OCAMLDEP kernel/subtyping.mli >OCAMLDEP kernel/conv_oracle.mli >OCAMLDEP kernel/indtypes.mli >OCAMLDEP kernel/vconv.mli >OCAMLDEP kernel/cemitcodes.mli >OCAMLDEP kernel/mod_subst.mli >OCAMLDEP kernel/retroknowledge.mli >OCAMLDEP kernel/vm.mli >OCAMLDEP kernel/mod_typing.mli >OCAMLDEP kernel/cbytegen.mli >OCAMLDEP kernel/reduction.mli >OCAMLDEP kernel/csymtable.mli >OCAMLDEP kernel/cbytecodes.mli >OCAMLDEP kernel/cooking.mli >OCAMLDEP kernel/typeops.mli >OCAMLDEP kernel/term_typing.mli >OCAMLDEP kernel/safe_typing.mli >OCAMLDEP kernel/closure.mli >OCAMLDEP kernel/entries.mli >OCAMLDEP kernel/names.mli >OCAMLDEP kernel/environ.mli >OCAMLDEP kernel/univ.mli >OCAMLDEP kernel/modops.mli >OCAMLDEP kernel/pre_env.mli >OCAMLDEP kernel/term.mli >OCAMLDEP kernel/inductive.mli >OCAMLDEP kernel/type_errors.mli >OCAMLDEP kernel/sign.mli >OCAMLDEP kernel/copcodes.ml >OCAMLDEP scripts/tolink.ml >OCAMLDEP ide/config_parser.ml >OCAMLDEP dev/ocamlweb-doc/syntax.ml >OCAMLDEP ide/config_lexer.ml >OCAMLDEP ide/highlight.ml >OCAMLDEP ide/find_phrase.ml >OCAMLDEP ide/extract_index.ml >OCAMLDEP ide/utf8_convert.ml >OCAMLDEP contrib/dp/dp_zenon.ml >OCAMLDEP tools/gallina_lexer.ml >OCAMLDEP tools/coqdep_lexer.ml >OCAMLDEP tools/coqwc.ml >OCAMLDEP tools/coqdoc/pretty.ml >OCAMLDEP tools/coqdoc/index.ml >OCAMLDEP dev/ocamlweb-doc/lex.ml >OCAMLDEP ide/command_windows.ml >OCAMLDEP ide/utils/configwin_html_config.ml >OCAMLDEP ide/utils/config_file.ml >OCAMLDEP ide/utils/configwin_keys.ml >OCAMLDEP ide/utils/configwin_messages.ml >OCAMLDEP ide/utils/configwin_ihm.ml >OCAMLDEP ide/utils/uoptions.ml >OCAMLDEP ide/utils/configwin.ml >OCAMLDEP ide/utils/editable_cells.ml >OCAMLDEP ide/utils/configwin_types.ml >OCAMLDEP ide/utils/okey.ml >OCAMLDEP ide/coqide.ml >OCAMLDEP ide/undo.ml >OCAMLDEP ide/coq.ml >OCAMLDEP ide/preferences.ml >OCAMLDEP ide/ideutils.ml >OCAMLDEP ide/coq_commands.ml >OCAMLDEP ide/blaster_window.ml >OCAMLDEP ide/coq_tactics.ml >OCAMLDEP checker/typeops.ml >OCAMLDEP checker/validate.ml >OCAMLDEP checker/check_stat.ml >OCAMLDEP checker/declarations.ml >OCAMLDEP checker/modops.ml >OCAMLDEP checker/closure.ml >OCAMLDEP checker/mod_checking.ml >OCAMLDEP checker/reduction.ml >OCAMLDEP checker/environ.ml >OCAMLDEP checker/main.ml >OCAMLDEP checker/indtypes.ml >OCAMLDEP checker/inductive.ml >OCAMLDEP checker/check.ml >OCAMLDEP checker/safe_typing.ml >OCAMLDEP checker/term.ml >OCAMLDEP checker/checker.ml >OCAMLDEP checker/type_errors.ml >OCAMLDEP checker/subtyping.ml >OCAMLDEP parsing/g_natsyntax.ml >OCAMLDEP parsing/g_intsyntax.ml >OCAMLDEP parsing/g_ascii_syntax.ml >OCAMLDEP parsing/g_string_syntax.ml >OCAMLDEP parsing/prettyp.ml >OCAMLDEP parsing/ppdecl_proof.ml >OCAMLDEP parsing/egrammar.ml >OCAMLDEP parsing/extend.ml >OCAMLDEP parsing/ppconstr.ml >OCAMLDEP parsing/ppvernac.ml >OCAMLDEP parsing/g_rsyntax.ml >OCAMLDEP parsing/search.ml >OCAMLDEP parsing/pptactic.ml >OCAMLDEP parsing/printmod.ml >OCAMLDEP parsing/g_zsyntax.ml >OCAMLDEP parsing/printer.ml >OCAMLDEP parsing/tactic_printer.ml >OCAMLDEP interp/syntax_def.ml >OCAMLDEP interp/constrintern.ml >OCAMLDEP interp/constrextern.ml >OCAMLDEP interp/coqlib.ml >OCAMLDEP interp/genarg.ml >OCAMLDEP interp/dumpglob.ml >OCAMLDEP interp/notation.ml >OCAMLDEP interp/ppextend.ml >OCAMLDEP interp/reserve.ml >OCAMLDEP interp/implicit_quantifiers.ml >OCAMLDEP interp/topconstr.ml >OCAMLDEP interp/modintern.ml >OCAMLDEP scripts/coqmktop.ml >OCAMLDEP scripts/coqc.ml >OCAMLDEP contrib/dp/dp.ml >OCAMLDEP contrib/dp/dp_why.ml >OCAMLDEP contrib/dp/dp_gappa.ml >OCAMLDEP contrib/micromega/sos.ml >OCAMLDEP contrib/micromega/mfourier.ml >OCAMLDEP contrib/micromega/micromega.ml >OCAMLDEP contrib/micromega/mutils.ml >OCAMLDEP contrib/micromega/csdpcert.ml >OCAMLDEP contrib/micromega/vector.ml >OCAMLDEP contrib/micromega/coq_micromega.ml >OCAMLDEP contrib/micromega/certificate.ml >OCAMLDEP contrib/omega/coq_omega.ml >OCAMLDEP contrib/omega/omega.ml >OCAMLDEP contrib/firstorder/unify.ml >OCAMLDEP contrib/firstorder/formula.ml >OCAMLDEP contrib/firstorder/instances.ml >OCAMLDEP contrib/firstorder/rules.ml >OCAMLDEP contrib/firstorder/ground.ml >OCAMLDEP contrib/firstorder/sequent.ml >OCAMLDEP contrib/funind/rawtermops.ml >OCAMLDEP contrib/funind/functional_principles_types.ml >OCAMLDEP contrib/funind/functional_principles_proofs.ml >OCAMLDEP contrib/funind/indfun.ml >OCAMLDEP contrib/funind/merge.ml >OCAMLDEP contrib/funind/invfun.ml >OCAMLDEP contrib/funind/rawterm_to_relation.ml >OCAMLDEP contrib/funind/indfun_common.ml >OCAMLDEP contrib/funind/recdef.ml >OCAMLDEP contrib/xml/proof2aproof.ml >OCAMLDEP contrib/xml/doubleTypeInference.ml >OCAMLDEP contrib/xml/cic2Xml.ml >OCAMLDEP contrib/xml/cic2acic.ml >OCAMLDEP contrib/xml/xmlcommand.ml >OCAMLDEP contrib/xml/acic.ml >OCAMLDEP contrib/xml/unshare.ml >OCAMLDEP contrib/subtac/eterm.ml >OCAMLDEP contrib/subtac/subtac_classes.ml >OCAMLDEP contrib/subtac/subtac_coercion.ml >OCAMLDEP contrib/subtac/subtac_utils.ml >OCAMLDEP contrib/subtac/subtac_cases.ml >OCAMLDEP contrib/subtac/subtac_pretyping_F.ml >OCAMLDEP contrib/subtac/subtac_obligations.ml >OCAMLDEP contrib/subtac/subtac_command.ml >OCAMLDEP contrib/subtac/subtac_errors.ml >OCAMLDEP contrib/subtac/subtac.ml >OCAMLDEP contrib/subtac/subtac_pretyping.ml >OCAMLDEP contrib/fourier/fourier.ml >OCAMLDEP contrib/fourier/fourierR.ml >OCAMLDEP contrib/romega/const_omega.ml >OCAMLDEP contrib/romega/refl_omega.ml >OCAMLDEP contrib/extraction/scheme.ml >OCAMLDEP contrib/extraction/common.ml >OCAMLDEP contrib/extraction/modutil.ml >OCAMLDEP contrib/extraction/table.ml >OCAMLDEP contrib/extraction/haskell.ml >OCAMLDEP contrib/extraction/ocaml.ml >OCAMLDEP contrib/extraction/extract_env.ml >OCAMLDEP contrib/extraction/mlutil.ml >OCAMLDEP contrib/extraction/extraction.ml >OCAMLDEP contrib/cc/ccalgo.ml >OCAMLDEP contrib/cc/ccproof.ml >OCAMLDEP contrib/cc/cctac.ml >OCAMLDEP contrib/interface/showproof_ct.ml >OCAMLDEP contrib/interface/xlate.ml >OCAMLDEP contrib/interface/history.ml >OCAMLDEP contrib/interface/dad.ml >OCAMLDEP contrib/interface/pbp.ml >OCAMLDEP contrib/interface/translate.ml >OCAMLDEP contrib/interface/paths.ml >OCAMLDEP contrib/interface/showproof.ml >OCAMLDEP contrib/interface/name_to_ast.ml >OCAMLDEP contrib/interface/depends.ml >OCAMLDEP contrib/interface/parse.ml >OCAMLDEP contrib/interface/vtp.ml >OCAMLDEP contrib/interface/blast.ml >OCAMLDEP contrib/rtauto/refl_tauto.ml >OCAMLDEP contrib/rtauto/proof_search.ml >OCAMLDEP contrib/ring/ring.ml >OCAMLDEP contrib/ring/quote.ml >OCAMLDEP tools/coqdoc/alpha.ml >OCAMLDEP tools/coqdoc/cdglobals.ml >OCAMLDEP tools/coqdoc/main.ml >OCAMLDEP tools/coqdoc/output.ml >OCAMLDEP tools/gallina.ml >OCAMLDEP tools/coqdep.ml >OCAMLDEP library/nameops.ml >OCAMLDEP library/declaremods.ml >OCAMLDEP library/decl_kinds.ml >OCAMLDEP library/libnames.ml >OCAMLDEP library/states.ml >OCAMLDEP library/lib.ml >OCAMLDEP library/libobject.ml >OCAMLDEP library/summary.ml >OCAMLDEP library/goptions.ml >OCAMLDEP library/declare.ml >OCAMLDEP library/impargs.ml >OCAMLDEP library/nametab.ml >OCAMLDEP library/heads.ml >OCAMLDEP library/library.ml >OCAMLDEP library/dischargedhypsmap.ml >OCAMLDEP library/global.ml >OCAMLDEP library/decls.ml >OCAMLDEP proofs/logic.ml >OCAMLDEP proofs/refiner.ml >OCAMLDEP proofs/redexpr.ml >OCAMLDEP proofs/proof_type.ml >OCAMLDEP proofs/tacexpr.ml >OCAMLDEP proofs/tactic_debug.ml >OCAMLDEP proofs/clenvtac.ml >OCAMLDEP proofs/tacmach.ml >OCAMLDEP proofs/evar_refiner.ml >OCAMLDEP proofs/proof_trees.ml >OCAMLDEP proofs/pfedit.ml >OCAMLDEP proofs/decl_mode.ml >OCAMLDEP tactics/nbtermdn.ml >OCAMLDEP tactics/termdn.ml >OCAMLDEP tactics/decl_interp.ml >OCAMLDEP tactics/refine.ml >OCAMLDEP tactics/btermdn.ml >OCAMLDEP tactics/tacinterp.ml >OCAMLDEP tactics/contradiction.ml >OCAMLDEP tactics/elim.ml >OCAMLDEP tactics/tactics.ml >OCAMLDEP tactics/hiddentac.ml >OCAMLDEP tactics/autorewrite.ml >OCAMLDEP tactics/dhyp.ml >OCAMLDEP tactics/evar_tactics.ml >OCAMLDEP tactics/inv.ml >OCAMLDEP tactics/equality.ml >OCAMLDEP tactics/tacticals.ml >OCAMLDEP tactics/leminv.ml >OCAMLDEP tactics/dn.ml >OCAMLDEP tactics/decl_proof_instr.ml >OCAMLDEP tactics/auto.ml >OCAMLDEP toplevel/classes.ml >OCAMLDEP toplevel/metasyntax.ml >OCAMLDEP toplevel/toplevel.ml >OCAMLDEP toplevel/usage.ml >OCAMLDEP toplevel/record.ml >OCAMLDEP toplevel/protectedtoplevel.ml >OCAMLDEP toplevel/line_oriented_parser.ml >OCAMLDEP toplevel/discharge.ml >OCAMLDEP toplevel/ind_tables.ml >OCAMLDEP toplevel/vernac.ml >OCAMLDEP toplevel/cerrors.ml >OCAMLDEP toplevel/vernacexpr.ml >OCAMLDEP toplevel/coqtop.ml >OCAMLDEP toplevel/command.ml >OCAMLDEP toplevel/vernacentries.ml >OCAMLDEP toplevel/class.ml >OCAMLDEP toplevel/vernacinterp.ml >OCAMLDEP toplevel/himsg.ml >OCAMLDEP toplevel/auto_ind_decl.ml >OCAMLDEP toplevel/coqinit.ml >OCAMLDEP lib/heap.ml >OCAMLDEP lib/envars.ml >OCAMLDEP lib/tlm.ml >OCAMLDEP lib/system.ml >OCAMLDEP lib/rtree.ml >OCAMLDEP lib/pp_control.ml >OCAMLDEP lib/predicate.ml >OCAMLDEP lib/edit.ml >OCAMLDEP lib/flags.ml >OCAMLDEP lib/hashcons.ml >OCAMLDEP lib/dyn.ml >OCAMLDEP lib/bigint.ml >OCAMLDEP lib/explore.ml >OCAMLDEP lib/option.ml >OCAMLDEP lib/gmap.ml >OCAMLDEP lib/profile.ml >OCAMLDEP lib/gmapl.ml >OCAMLDEP lib/bstack.ml >OCAMLDEP lib/util.ml >OCAMLDEP lib/gset.ml >OCAMLDEP config/coq_config.ml >OCAMLDEP config/giveostype.ml >OCAMLDEP theories/Numbers/Natural/BigN/NMake_gen.ml >OCAMLDEP dev/db_printers.ml >OCAMLDEP dev/ocamlweb-doc/ast.ml >OCAMLDEP dev/ocamlweb-doc/parse.ml >OCAMLDEP dev/vm_printers.ml >OCAMLDEP dev/top_printers.ml >OCAMLDEP pretyping/cases.ml >OCAMLDEP pretyping/detyping.ml >OCAMLDEP pretyping/termops.ml >OCAMLDEP pretyping/typeclasses_errors.ml >OCAMLDEP pretyping/indrec.ml >OCAMLDEP pretyping/clenv.ml >OCAMLDEP pretyping/rawterm.ml >OCAMLDEP pretyping/pretyping.ml >OCAMLDEP pretyping/matching.ml >OCAMLDEP pretyping/classops.ml >OCAMLDEP pretyping/evd.ml >OCAMLDEP pretyping/typeclasses.ml >OCAMLDEP pretyping/pretype_errors.ml >OCAMLDEP pretyping/evarutil.ml >OCAMLDEP pretyping/evarconv.ml >OCAMLDEP pretyping/vnorm.ml >OCAMLDEP pretyping/unification.ml >OCAMLDEP pretyping/coercion.ml >OCAMLDEP pretyping/tacred.ml >OCAMLDEP pretyping/reductionops.ml >OCAMLDEP pretyping/retyping.ml >OCAMLDEP pretyping/recordops.ml >OCAMLDEP pretyping/inductiveops.ml >OCAMLDEP pretyping/pattern.ml >OCAMLDEP pretyping/cbv.ml >OCAMLDEP pretyping/typing.ml >OCAMLDEP kernel/typeops.ml >OCAMLDEP kernel/mod_subst.ml >OCAMLDEP kernel/vconv.ml >OCAMLDEP kernel/esubst.ml >OCAMLDEP kernel/declarations.ml >OCAMLDEP kernel/names.ml >OCAMLDEP kernel/entries.ml >OCAMLDEP kernel/modops.ml >OCAMLDEP kernel/sign.ml >OCAMLDEP kernel/closure.ml >OCAMLDEP kernel/term_typing.ml >OCAMLDEP kernel/cbytegen.ml >OCAMLDEP kernel/mod_typing.ml >OCAMLDEP kernel/univ.ml >OCAMLDEP kernel/reduction.ml >OCAMLDEP kernel/environ.ml >OCAMLDEP kernel/vm.ml >OCAMLDEP kernel/cbytecodes.ml >OCAMLDEP kernel/indtypes.ml >OCAMLDEP kernel/inductive.ml >OCAMLDEP kernel/cooking.ml >OCAMLDEP kernel/safe_typing.ml >OCAMLDEP kernel/csymtable.ml >OCAMLDEP kernel/retroknowledge.ml >OCAMLDEP kernel/conv_oracle.ml >OCAMLDEP kernel/cemitcodes.ml >OCAMLDEP kernel/term.ml >OCAMLDEP kernel/type_errors.ml >OCAMLDEP kernel/pre_env.ml >OCAMLDEP kernel/subtyping.ml >CAMLP4DEPS parsing/g_decl_mode.ml4 >CAMLP4DEPS parsing/g_vernac.ml4 >CAMLP4DEPS parsing/g_xml.ml4 >CAMLP4DEPS parsing/g_proofs.ml4 >CAMLP4DEPS contrib/dp/g_dp.ml4 >CAMLP4DEPS contrib/micromega/g_micromega.ml4 >CAMLP4DEPS contrib/omega/g_omega.ml4 >CAMLP4DEPS contrib/firstorder/g_ground.ml4 >CAMLP4DEPS contrib/funind/g_indfun.ml4 >CAMLP4DEPS contrib/xml/acic2Xml.ml4 >CAMLP4DEPS contrib/xml/xmlentries.ml4 >CAMLP4DEPS contrib/xml/xml.ml4 >CAMLP4DEPS contrib/xml/dumptree.ml4 >CAMLP4DEPS contrib/xml/proofTree2Xml.ml4 >CAMLP4DEPS contrib/subtac/g_subtac.ml4 >CAMLP4DEPS contrib/subtac/g_eterm.ml4 >CAMLP4DEPS contrib/subtac/equations.ml4 >CAMLP4DEPS contrib/fourier/g_fourier.ml4 >CAMLP4DEPS contrib/romega/g_romega.ml4 >CAMLP4DEPS contrib/extraction/g_extraction.ml4 >CAMLP4DEPS contrib/cc/g_congruence.ml4 >CAMLP4DEPS contrib/field/field.ml4 >CAMLP4DEPS contrib/interface/centaur.ml4 >CAMLP4DEPS contrib/interface/line_parser.ml4 >CAMLP4DEPS contrib/interface/debug_tac.ml4 >CAMLP4DEPS contrib/rtauto/g_rtauto.ml4 >CAMLP4DEPS contrib/ring/g_ring.ml4 >CAMLP4DEPS contrib/ring/g_quote.ml4 >CAMLP4DEPS contrib/setoid_ring/newring.ml4 >CAMLP4DEPS tools/coq_makefile.ml4 >CAMLP4DEPS tools/coq-tex.ml4 >CAMLP4DEPS tactics/extraargs.ml4 >CAMLP4DEPS tactics/eauto.ml4 >CAMLP4DEPS tactics/class_tactics.ml4 >CAMLP4DEPS tactics/extratactics.ml4 >CAMLP4DEPS tactics/tauto.ml4 >CAMLP4DEPS tactics/eqdecide.ml4 >CAMLP4DEPS tactics/hipattern.ml4 >CAMLP4DEPS toplevel/whelp.ml4 >CAMLP4DEPS toplevel/mltop.ml4 >rm toplevel/mltop.ml contrib/xml/xml.ml tactics/tauto.ml tactics/class_tactics.ml tools/coq-tex.ml parsing/g_vernac.ml contrib/xml/proofTree2Xml.ml contrib/subtac/equations.ml tactics/eqdecide.ml tools/coq_makefile.ml toplevel/whelp.ml parsing/g_ltac.ml contrib/cc/g_congruence.ml parsing/q_coqast.ml contrib/xml/xmlentries.ml lib/compat.ml parsing/q_constr.ml contrib/setoid_ring/newring.ml contrib/subtac/g_eterm.ml tactics/extraargs.ml contrib/subtac/g_subtac.ml parsing/g_decl_mode.ml contrib/interface/centaur.ml contrib/omega/g_omega.ml parsing/vernacextend.ml contrib/micromega/g_micromega.ml contrib/field/field.ml contrib/ring/g_quote.ml tactics/hipattern.ml parsing/g_tactic.ml parsing/g_constr.ml contrib/interface/debug_tac.ml contrib/firstorder/g_ground.ml parsing/tacextend.ml parsing/pcoq.ml contrib/funind/g_indfun.ml contrib/extraction/g_extraction.ml parsing/g_xml.ml contrib/romega/g_romega.ml lib/pp.ml tactics/eauto.ml contrib/xml/dumptree.ml contrib/interface/line_parser.ml tactics/extratactics.ml parsing/argextend.ml parsing/lexer.ml parsing/q_util.ml parsing/g_proofs.ml contrib/xml/acic2Xml.ml contrib/ring/g_ring.ml contrib/fourier/g_fourier.ml parsing/g_prim.ml contrib/rtauto/g_rtauto.ml contrib/dp/g_dp.ml >make[1]: Leaving directory `/var/tmp/portage/sci-mathematics/coq-8.2_p1-r1/work/coq-8.2pl1' >make[1]: Entering directory `/var/tmp/portage/sci-mathematics/coq-8.2_p1-r1/work/coq-8.2pl1' >OCAMLC config/coq_config.mli >OCAMLC config/coq_config.ml >OCAMLC lib/pp_control.mli >OCAMLC lib/pp_control.ml >OCAMLC lib/pp.mli >OCAMLC4 lib/pp.ml4 >OCAMLC4 lib/compat.ml4 >OCAMLC lib/flags.mli >OCAMLC lib/flags.ml >OCAMLC lib/util.mli >OCAMLC lib/util.ml >OCAMLC lib/bigint.mli >OCAMLC lib/bigint.ml >OCAMLC lib/dyn.mli >OCAMLC lib/dyn.ml >OCAMLC lib/hashcons.mli >OCAMLC lib/hashcons.ml >OCAMLC lib/predicate.mli >OCAMLC lib/predicate.ml >OCAMLC lib/rtree.mli >OCAMLC lib/rtree.ml >OCAMLC lib/option.mli >OCAMLC lib/option.ml >OCAMLC kernel/names.mli >OCAMLC kernel/names.ml >OCAMLC kernel/univ.mli >OCAMLC kernel/univ.ml >OCAMLC kernel/esubst.mli >OCAMLC kernel/esubst.ml >OCAMLC kernel/term.mli >OCAMLC -rectypes kernel/term.ml >OCAMLC kernel/mod_subst.mli >OCAMLC kernel/mod_subst.ml >OCAMLC kernel/sign.mli >OCAMLC kernel/sign.ml >OCAMLC kernel/cbytecodes.mli >OCAMLC kernel/cbytecodes.ml >OCAMLC kernel/copcodes.ml >OCAMLC kernel/cemitcodes.mli >OCAMLC kernel/cemitcodes.ml >OCAMLC kernel/retroknowledge.mli >OCAMLC kernel/declarations.mli >OCAMLC kernel/declarations.ml >OCAMLC kernel/retroknowledge.ml >OCAMLC kernel/pre_env.mli >OCAMLC kernel/pre_env.ml >OCAMLC kernel/cbytegen.mli >OCAMLC kernel/cbytegen.ml >OCAMLC kernel/conv_oracle.mli >OCAMLC kernel/conv_oracle.ml >OCAMLC kernel/environ.mli >OCAMLC kernel/environ.ml >OCAMLC kernel/closure.mli >OCAMLC kernel/closure.ml >OCAMLC kernel/reduction.mli >OCAMLC kernel/reduction.ml >OCAMLC kernel/type_errors.mli >OCAMLC kernel/type_errors.ml >OCAMLC kernel/entries.mli >OCAMLC kernel/entries.ml >OCAMLC kernel/modops.mli >OCAMLC kernel/modops.ml >OCAMLC kernel/inductive.mli >OCAMLC kernel/inductive.ml >OCAMLC kernel/typeops.mli >OCAMLC kernel/typeops.ml >OCAMLC kernel/indtypes.mli >OCAMLC kernel/indtypes.ml >OCAMLC kernel/cooking.mli >OCAMLC kernel/cooking.ml >OCAMLC kernel/term_typing.mli >OCAMLC kernel/term_typing.ml >OCAMLC kernel/subtyping.mli >OCAMLC kernel/subtyping.ml >OCAMLC kernel/mod_typing.mli >OCAMLC kernel/mod_typing.ml >OCAMLC kernel/safe_typing.mli >OCAMLC kernel/safe_typing.ml >OCAMLC library/nameops.mli >OCAMLC library/nameops.ml >OCAMLC library/libnames.mli >OCAMLC library/libnames.ml >OCAMLC library/summary.mli >OCAMLC library/summary.ml >OCAMLC library/nametab.mli >OCAMLC -rectypes library/nametab.ml >OCAMLC library/libobject.mli >OCAMLC library/libobject.ml >OCAMLC library/lib.mli >OCAMLC library/lib.ml >OCAMLC library/goptions.mli >OCAMLC library/goptions.ml >OCAMLC library/decl_kinds.mli >OCAMLC library/decl_kinds.ml >OCAMLC library/global.mli >OCAMLC library/global.ml >OCAMLC pretyping/termops.mli >OCAMLC pretyping/termops.ml >OCAMLC pretyping/evd.mli >OCAMLC pretyping/evd.ml >OCAMLC pretyping/reductionops.mli >OCAMLC pretyping/reductionops.ml >OCAMLC pretyping/inductiveops.mli >OCAMLC pretyping/inductiveops.ml >OCAMLC pretyping/rawterm.mli >OCAMLC pretyping/rawterm.ml >OCAMLC pretyping/detyping.mli >OCAMLC pretyping/detyping.ml >OCAMLC pretyping/pattern.mli >OCAMLC pretyping/pattern.ml >OCAMLC interp/topconstr.mli >OCAMLC interp/topconstr.ml >OCAMLC interp/ppextend.mli >OCAMLC pretyping/classops.mli >OCAMLC interp/notation.mli >OCAMLC interp/genarg.mli >OCAMLC interp/genarg.ml >OCAMLC interp/ppextend.ml >OCAMLC -rectypes proofs/tacexpr.ml >OCAMLC parsing/lexer.mli >OCAMLC4 parsing/lexer.ml4 >OCAMLC parsing/extend.mli >OCAMLC parsing/extend.ml >OCAMLC proofs/decl_expr.mli >OCAMLC toplevel/vernacexpr.ml >OCAMLC parsing/pcoq.mli >OCAMLC4 parsing/pcoq.ml4 >OCAMLC parsing/q_util.mli >OCAMLC4 parsing/q_util.ml4 >OCAMLC4 parsing/q_coqast.ml4 >OCAMLC4 parsing/argextend.ml4 >OCAMLC4 parsing/tacextend.ml4 >OCAMLC4 parsing/vernacextend.ml4 >OCAMLC4 parsing/g_prim.ml4 >OCAMLC4 parsing/g_tactic.ml4 >OCAMLC4 parsing/g_ltac.ml4 >OCAMLC4 parsing/g_constr.ml4 >Testing parsing/grammar.cma >OCAMLC -a parsing/grammar.cma >OCAMLC4 parsing/q_constr.ml4 >make[1]: Leaving directory `/var/tmp/portage/sci-mathematics/coq-8.2_p1-r1/work/coq-8.2pl1' >***************************************************** >***************************************************** >****************** Entering stage2 ****************** >***************************************************** >***************************************************** >make -f Makefile.stage2 "stage2" >make[1]: Entering directory `/var/tmp/portage/sci-mathematics/coq-8.2_p1-r1/work/coq-8.2pl1' >TOUCH lib/pp.ml >TOUCH lib/compat.ml >TOUCH toplevel/mltop.ml >TOUCH toplevel/whelp.ml >TOUCH tactics/hipattern.ml >TOUCH tactics/eqdecide.ml >TOUCH tactics/tauto.ml >TOUCH tactics/extratactics.ml >TOUCH tactics/class_tactics.ml >TOUCH tactics/eauto.ml >TOUCH tactics/extraargs.ml >TOUCH tools/coq-tex.ml >TOUCH tools/coq_makefile.ml >TOUCH contrib/setoid_ring/newring.ml >TOUCH contrib/ring/g_quote.ml >TOUCH contrib/ring/g_ring.ml >TOUCH contrib/rtauto/g_rtauto.ml >TOUCH contrib/interface/debug_tac.ml >TOUCH contrib/interface/line_parser.ml >TOUCH contrib/interface/centaur.ml >TOUCH contrib/field/field.ml >TOUCH contrib/cc/g_congruence.ml >TOUCH contrib/extraction/g_extraction.ml >TOUCH contrib/romega/g_romega.ml >TOUCH contrib/fourier/g_fourier.ml >TOUCH contrib/subtac/equations.ml >TOUCH contrib/subtac/g_eterm.ml >TOUCH contrib/subtac/g_subtac.ml >TOUCH contrib/xml/proofTree2Xml.ml >TOUCH contrib/xml/dumptree.ml >TOUCH contrib/xml/xml.ml >TOUCH contrib/xml/xmlentries.ml >TOUCH contrib/xml/acic2Xml.ml >TOUCH contrib/funind/g_indfun.ml >TOUCH contrib/firstorder/g_ground.ml >TOUCH contrib/omega/g_omega.ml >TOUCH contrib/micromega/g_micromega.ml >TOUCH contrib/dp/g_dp.ml >TOUCH parsing/g_proofs.ml >TOUCH parsing/g_ltac.ml >TOUCH parsing/g_tactic.ml >TOUCH parsing/q_coqast.ml >TOUCH parsing/g_constr.ml >TOUCH parsing/argextend.ml >TOUCH parsing/g_xml.ml >TOUCH parsing/q_util.ml >TOUCH parsing/g_vernac.ml >TOUCH parsing/tacextend.ml >TOUCH parsing/q_constr.ml >TOUCH parsing/lexer.ml >TOUCH parsing/pcoq.ml >TOUCH parsing/g_prim.ml >TOUCH parsing/vernacextend.ml >TOUCH parsing/g_decl_mode.ml >OCAMLDEP4 parsing/g_decl_mode.ml4 >OCAMLDEP4 parsing/g_vernac.ml4 >OCAMLDEP4 parsing/g_xml.ml4 >OCAMLDEP4 parsing/g_proofs.ml4 >OCAMLDEP4 contrib/dp/g_dp.ml4 >OCAMLDEP4 contrib/micromega/g_micromega.ml4 >OCAMLDEP4 contrib/omega/g_omega.ml4 >OCAMLDEP4 contrib/firstorder/g_ground.ml4 >OCAMLDEP4 contrib/funind/g_indfun.ml4 >OCAMLDEP4 contrib/xml/acic2Xml.ml4 >OCAMLDEP4 contrib/xml/xmlentries.ml4 >OCAMLDEP4 contrib/xml/xml.ml4 >OCAMLDEP4 contrib/xml/dumptree.ml4 >OCAMLDEP4 contrib/xml/proofTree2Xml.ml4 >OCAMLDEP4 contrib/subtac/g_subtac.ml4 >OCAMLDEP4 contrib/subtac/g_eterm.ml4 >OCAMLDEP4 contrib/subtac/equations.ml4 >OCAMLDEP4 contrib/fourier/g_fourier.ml4 >OCAMLDEP4 contrib/romega/g_romega.ml4 >OCAMLDEP4 contrib/extraction/g_extraction.ml4 >OCAMLDEP4 contrib/cc/g_congruence.ml4 >OCAMLDEP4 contrib/field/field.ml4 >OCAMLDEP4 contrib/interface/centaur.ml4 >OCAMLDEP4 contrib/interface/line_parser.ml4 >OCAMLDEP4 contrib/interface/debug_tac.ml4 >OCAMLDEP4 contrib/rtauto/g_rtauto.ml4 >OCAMLDEP4 contrib/ring/g_ring.ml4 >OCAMLDEP4 contrib/ring/g_quote.ml4 >OCAMLDEP4 contrib/setoid_ring/newring.ml4 >OCAMLDEP4 tools/coq_makefile.ml4 >OCAMLDEP4 tools/coq-tex.ml4 >OCAMLDEP4 tactics/extraargs.ml4 >OCAMLDEP4 tactics/eauto.ml4 >OCAMLDEP4 tactics/class_tactics.ml4 >OCAMLDEP4 tactics/extratactics.ml4 >OCAMLDEP4 tactics/tauto.ml4 >OCAMLDEP4 tactics/eqdecide.ml4 >OCAMLDEP4 tactics/hipattern.ml4 >OCAMLDEP4 toplevel/whelp.ml4 >OCAMLDEP4 toplevel/mltop.ml4 >rm contrib/xml/xml.ml tactics/tauto.ml tactics/class_tactics.ml parsing/g_vernac.ml parsing/g_prim.ml contrib/rtauto/g_rtauto.ml contrib/subtac/equations.ml tactics/eqdecide.ml lib/pp.ml toplevel/whelp.ml contrib/romega/g_romega.ml parsing/g_ltac.ml contrib/cc/g_congruence.ml parsing/q_coqast.ml contrib/xml/xmlentries.ml lib/compat.ml parsing/q_constr.ml contrib/setoid_ring/newring.ml contrib/subtac/g_eterm.ml tactics/extraargs.ml contrib/subtac/g_subtac.ml parsing/g_decl_mode.ml contrib/interface/centaur.ml contrib/xml/proofTree2Xml.ml tools/coq_makefile.ml parsing/vernacextend.ml contrib/field/field.ml contrib/ring/g_quote.ml tactics/hipattern.ml parsing/g_tactic.ml contrib/omega/g_omega.ml parsing/g_constr.ml contrib/interface/debug_tac.ml contrib/firstorder/g_ground.ml parsing/pcoq.ml parsing/tacextend.ml contrib/funind/g_indfun.ml contrib/xml/dumptree.ml contrib/extraction/g_extraction.ml parsing/g_xml.ml tactics/eauto.ml contrib/interface/line_parser.ml tools/coq-tex.ml tactics/extratactics.ml parsing/argextend.ml contrib/micromega/g_micromega.ml parsing/lexer.ml parsing/q_util.ml toplevel/mltop.ml parsing/g_proofs.ml contrib/xml/acic2Xml.ml contrib/ring/g_ring.ml contrib/fourier/g_fourier.ml contrib/dp/g_dp.ml >make[1]: Leaving directory `/var/tmp/portage/sci-mathematics/coq-8.2_p1-r1/work/coq-8.2pl1' >make[1]: Entering directory `/var/tmp/portage/sci-mathematics/coq-8.2_p1-r1/work/coq-8.2pl1' >OCAMLOPT config/coq_config.ml >OCAMLOPT lib/pp_control.ml >OCAMLOPT4 lib/pp.ml4 >OCAMLOPT4 lib/compat.ml4 >OCAMLOPT lib/flags.ml >OCAMLOPT lib/util.ml >OCAMLC lib/system.mli >OCAMLOPT lib/system.ml >OCAMLC lib/envars.mli >OCAMLOPT lib/envars.ml >OCAMLOPT tools/coqdep_lexer.ml >OCAMLOPT tools/coqdep.ml >OCAMLOPT -o bin/coqdep >true bin/coqdep >make[1]: Leaving directory `/var/tmp/portage/sci-mathematics/coq-8.2_p1-r1/work/coq-8.2pl1' >***************************************************** >***************************************************** >****************** Entering stage3 ****************** >***************************************************** >***************************************************** >make -f Makefile.stage3 "world" >make[1]: Entering directory `/var/tmp/portage/sci-mathematics/coq-8.2_p1-r1/work/coq-8.2pl1' >COQDEP contrib/dp/Dp.v >COQDEP contrib/setoid_ring/RealField.v >COQDEP contrib/setoid_ring/Field.v >COQDEP contrib/setoid_ring/Field_tac.v >COQDEP contrib/setoid_ring/Field_theory.v >COQDEP contrib/setoid_ring/ZArithRing.v >COQDEP contrib/setoid_ring/NArithRing.v >COQDEP contrib/setoid_ring/ArithRing.v >COQDEP contrib/setoid_ring/Ring.v >COQDEP contrib/setoid_ring/Ring_equiv.v >COQDEP contrib/setoid_ring/InitialRing.v >COQDEP contrib/setoid_ring/Ring_base.v >COQDEP contrib/setoid_ring/Ring_tac.v >COQDEP contrib/setoid_ring/Ring_polynom.v >COQDEP contrib/setoid_ring/Ring_theory.v >COQDEP contrib/setoid_ring/BinList.v >COQDEP contrib/funind/Recdef.v >COQDEP contrib/rtauto/Rtauto.v >COQDEP contrib/rtauto/Bintree.v >COQDEP contrib/fourier/Fourier.v >COQDEP contrib/fourier/Fourier_util.v >COQDEP contrib/field/LegacyField.v >COQDEP contrib/field/LegacyField_Tactic.v >COQDEP contrib/field/LegacyField_Theory.v >COQDEP contrib/field/LegacyField_Compl.v >COQDEP contrib/ring/Setoid_ring_theory.v >COQDEP contrib/ring/Setoid_ring.v >COQDEP contrib/ring/Setoid_ring_normalize.v >COQDEP contrib/ring/Quote.v >COQDEP contrib/ring/Ring_abstract.v >COQDEP contrib/ring/LegacyZArithRing.v >COQDEP contrib/ring/LegacyNArithRing.v >COQDEP contrib/ring/LegacyRing.v >COQDEP contrib/ring/LegacyRing_theory.v >COQDEP contrib/ring/Ring_normalize.v >COQDEP contrib/ring/LegacyArithRing.v >COQDEP contrib/micromega/Tauto.v >COQDEP contrib/micromega/RMicromega.v >COQDEP contrib/micromega/QMicromega.v >COQDEP contrib/micromega/ZMicromega.v >COQDEP contrib/micromega/Psatz.v >COQDEP contrib/micromega/ZCoeff.v >COQDEP contrib/micromega/OrderedRing.v >COQDEP contrib/micromega/VarMap.v >COQDEP contrib/micromega/EnvRing.v >COQDEP contrib/micromega/RingMicromega.v >COQDEP contrib/micromega/Env.v >COQDEP contrib/micromega/Refl.v >COQDEP contrib/micromega/CheckerMaker.v >COQDEP contrib/romega/ROmega.v >COQDEP contrib/romega/ReflOmegaCore.v >COQDEP contrib/omega/Omega.v >COQDEP contrib/omega/OmegaLemmas.v >COQDEP contrib/omega/PreOmega.v >COQDEP theories/Program/Program.v >COQDEP theories/Program/Syntax.v >COQDEP theories/Program/Combinators.v >COQDEP theories/Program/Basics.v >COQDEP theories/Program/Wf.v >COQDEP theories/Program/Utils.v >COQDEP theories/Program/Subset.v >COQDEP theories/Program/Equality.v >COQDEP theories/Program/Tactics.v >COQDEP theories/Classes/SetoidDec.v >COQDEP theories/Classes/EquivDec.v >COQDEP theories/Classes/SetoidAxioms.v >COQDEP theories/Classes/SetoidClass.v >COQDEP theories/Classes/SetoidTactics.v >COQDEP theories/Classes/Equivalence.v >COQDEP theories/Classes/Functions.v >COQDEP theories/Classes/Morphisms_Relations.v >COQDEP theories/Classes/Morphisms_Prop.v >COQDEP theories/Classes/Morphisms.v >COQDEP theories/Classes/RelationClasses.v >COQDEP theories/Classes/Init.v >COQDEP theories/Unicode/Utf8.v >COQDEP theories/Numbers/Rational/BigQ/BigQ.v >COQDEP theories/Numbers/Rational/BigQ/QMake.v >COQDEP theories/Numbers/Rational/SpecViaQ/QSig.v >COQDEP theories/Numbers/Cyclic/ZModulo/ZModulo.v >COQDEP theories/Numbers/Cyclic/DoubleCyclic/DoubleCyclic.v >COQDEP theories/Numbers/Cyclic/DoubleCyclic/DoubleLift.v >COQDEP theories/Numbers/Cyclic/DoubleCyclic/DoubleSqrt.v >COQDEP theories/Numbers/Cyclic/DoubleCyclic/DoubleDiv.v >COQDEP theories/Numbers/Cyclic/DoubleCyclic/DoubleDivn1.v >COQDEP theories/Numbers/Cyclic/DoubleCyclic/DoubleMul.v >COQDEP theories/Numbers/Cyclic/DoubleCyclic/DoubleSub.v >COQDEP theories/Numbers/Cyclic/DoubleCyclic/DoubleAdd.v >COQDEP theories/Numbers/Cyclic/DoubleCyclic/DoubleBase.v >COQDEP theories/Numbers/Cyclic/DoubleCyclic/DoubleType.v >COQDEP theories/Numbers/Cyclic/Int31/Cyclic31.v >COQDEP theories/Numbers/Cyclic/Int31/Int31.v >COQDEP theories/Numbers/Cyclic/Abstract/NZCyclic.v >COQDEP theories/Numbers/Cyclic/Abstract/CyclicAxioms.v >COQDEP theories/Numbers/NatInt/NZMulOrder.v >COQDEP theories/Numbers/NatInt/NZAddOrder.v >COQDEP theories/Numbers/NatInt/NZOrder.v >COQDEP theories/Numbers/NatInt/NZMul.v >COQDEP theories/Numbers/NatInt/NZAdd.v >COQDEP theories/Numbers/NatInt/NZBase.v >COQDEP theories/Numbers/NatInt/NZAxioms.v >COQDEP theories/Numbers/Integer/BigZ/BigZ.v >COQDEP theories/Numbers/Integer/BigZ/ZMake.v >COQDEP theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v >COQDEP theories/Numbers/Integer/SpecViaZ/ZSig.v >COQDEP theories/Numbers/Integer/NatPairs/ZNatPairs.v >COQDEP theories/Numbers/Integer/Binary/ZBinary.v >COQDEP theories/Numbers/Integer/Abstract/ZMulOrder.v >COQDEP theories/Numbers/Integer/Abstract/ZAddOrder.v >COQDEP theories/Numbers/Integer/Abstract/ZLt.v >COQDEP theories/Numbers/Integer/Abstract/ZMul.v >COQDEP theories/Numbers/Integer/Abstract/ZAdd.v >COQDEP theories/Numbers/Integer/Abstract/ZBase.v >COQDEP theories/Numbers/Integer/Abstract/ZAxioms.v >COQDEP theories/Numbers/Natural/BigN/BigN.v >COQDEP theories/Numbers/Natural/BigN/NMake.v >COQDEP theories/Numbers/Natural/BigN/Nbasic.v >COQDEP theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v >COQDEP theories/Numbers/Natural/SpecViaZ/NSig.v >COQDEP theories/Numbers/Natural/Binary/NBinary.v >COQDEP theories/Numbers/Natural/Binary/NBinDefs.v >COQDEP theories/Numbers/Natural/Peano/NPeano.v >COQDEP theories/Numbers/Natural/Abstract/NIso.v >COQDEP theories/Numbers/Natural/Abstract/NSub.v >COQDEP theories/Numbers/Natural/Abstract/NMulOrder.v >COQDEP theories/Numbers/Natural/Abstract/NAddOrder.v >COQDEP theories/Numbers/Natural/Abstract/NOrder.v >COQDEP theories/Numbers/Natural/Abstract/NMul.v >COQDEP theories/Numbers/Natural/Abstract/NAdd.v >COQDEP theories/Numbers/Natural/Abstract/NBase.v >COQDEP theories/Numbers/Natural/Abstract/NAxioms.v >COQDEP theories/Numbers/BigNumPrelude.v >COQDEP theories/Numbers/NumPrelude.v >COQDEP theories/Numbers/NaryFunctions.v >COQDEP theories/QArith/Qround.v >COQDEP theories/QArith/Qabs.v >COQDEP theories/QArith/Qpower.v >COQDEP theories/QArith/Qfield.v >COQDEP theories/QArith/Qcanon.v >COQDEP theories/QArith/QArith.v >COQDEP theories/QArith/Qreals.v >COQDEP theories/QArith/Qring.v >COQDEP theories/QArith/Qreduction.v >COQDEP theories/QArith/QArith_base.v >COQDEP theories/Sorting/PermutEq.v >COQDEP theories/Sorting/PermutSetoid.v >COQDEP theories/Sorting/Sorting.v >COQDEP theories/Sorting/Permutation.v >COQDEP theories/Sorting/Heap.v >COQDEP theories/Reals/Reals.v >COQDEP theories/Reals/Rlogic.v >COQDEP theories/Reals/Integration.v >COQDEP theories/Reals/RiemannInt.v >COQDEP theories/Reals/RiemannInt_SF.v >COQDEP theories/Reals/NewtonInt.v >COQDEP theories/Reals/Ranalysis.v >COQDEP theories/Reals/Rpower.v >COQDEP theories/Reals/Ranalysis4.v >COQDEP theories/Reals/Sqrt_reg.v >COQDEP theories/Reals/Rgeom.v >COQDEP theories/Reals/Rtrigo_calc.v >COQDEP theories/Reals/R_sqrt.v >COQDEP theories/Reals/Rsqrt_def.v >COQDEP theories/Reals/Rtrigo_reg.v >COQDEP theories/Reals/Exp_prop.v >COQDEP theories/Reals/PSeries_reg.v >COQDEP theories/Reals/MVT.v >COQDEP theories/Reals/Rtopology.v >COQDEP theories/Reals/Ranalysis3.v >COQDEP theories/Reals/Ranalysis2.v >COQDEP theories/Reals/Ranalysis1.v >COQDEP theories/Reals/RList.v >COQDEP theories/Reals/Rderiv.v >COQDEP theories/Reals/Rlimit.v >COQDEP theories/Reals/Rtrigo.v >COQDEP theories/Reals/Cos_plus.v >COQDEP theories/Reals/Cos_rel.v >COQDEP theories/Reals/Rtrigo_alt.v >COQDEP theories/Reals/Rtrigo_def.v >COQDEP theories/Reals/Rtrigo_fun.v >COQDEP theories/Reals/SeqSeries.v >COQDEP theories/Reals/Alembert.v >COQDEP theories/Reals/Cauchy_prod.v >COQDEP theories/Reals/Rprod.v >COQDEP theories/Reals/Rsigma.v >COQDEP theories/Reals/Binomial.v >COQDEP theories/Reals/AltSeries.v >COQDEP theories/Reals/PartSum.v >COQDEP theories/Reals/Rcomplete.v >COQDEP theories/Reals/SeqProp.v >COQDEP theories/Reals/Rseries.v >COQDEP theories/Reals/Rfunctions.v >COQDEP theories/Reals/ArithProp.v >COQDEP theories/Reals/SplitRmult.v >COQDEP theories/Reals/SplitAbsolu.v >COQDEP theories/Reals/R_sqr.v >COQDEP theories/Reals/Rbasic_fun.v >COQDEP theories/Reals/R_Ifp.v >COQDEP theories/Reals/Rpow_def.v >COQDEP theories/Reals/LegacyRfield.v >COQDEP theories/Reals/Rbase.v >COQDEP theories/Reals/DiscrR.v >COQDEP theories/Reals/RIneq.v >COQDEP theories/Reals/Raxioms.v >COQDEP theories/Reals/Rdefinitions.v >COQDEP theories/Wellfounded/Lexicographic_Exponentiation.v >COQDEP theories/Wellfounded/Lexicographic_Product.v >COQDEP theories/Wellfounded/Well_Ordering.v >COQDEP theories/Wellfounded/Wellfounded.v >COQDEP theories/Wellfounded/Union.v >COQDEP theories/Wellfounded/Transitive_Closure.v >COQDEP theories/Wellfounded/Inverse_Image.v >COQDEP theories/Wellfounded/Inclusion.v >COQDEP theories/Wellfounded/Disjoint_Union.v >COQDEP theories/Relations/Relations.v >COQDEP theories/Relations/Relation_Operators.v >COQDEP theories/Relations/Relation_Definitions.v >COQDEP theories/Relations/Operators_Properties.v >COQDEP theories/FSets/FMapFullAVL.v >COQDEP theories/FSets/FMapAVL.v >COQDEP theories/FSets/FSetFullAVL.v >COQDEP theories/FSets/FMaps.v >COQDEP theories/FSets/FSetToFiniteSet.v >COQDEP theories/FSets/FMapPositive.v >COQDEP theories/FSets/FMapWeakList.v >COQDEP theories/FSets/FMapFacts.v >COQDEP theories/FSets/FMapList.v >COQDEP theories/FSets/FMapInterface.v >COQDEP theories/FSets/FSets.v >COQDEP theories/FSets/FSetDecide.v >COQDEP theories/FSets/FSetAVL.v >COQDEP theories/FSets/FSetWeakList.v >COQDEP theories/FSets/FSetEqProperties.v >COQDEP theories/FSets/FSetProperties.v >COQDEP theories/FSets/FSetFacts.v >COQDEP theories/FSets/FSetBridge.v >COQDEP theories/FSets/FSetList.v >COQDEP theories/FSets/FSetInterface.v >COQDEP theories/FSets/OrderedTypeAlt.v >COQDEP theories/FSets/OrderedTypeEx.v >COQDEP theories/FSets/OrderedType.v >COQDEP theories/Sets/Uniset.v >COQDEP theories/Sets/Partial_Order.v >COQDEP theories/Sets/Relations_3_facts.v >COQDEP theories/Sets/Multiset.v >COQDEP theories/Sets/Relations_3.v >COQDEP theories/Sets/Integers.v >COQDEP theories/Sets/Relations_2_facts.v >COQDEP theories/Sets/Infinite_sets.v >COQDEP theories/Sets/Relations_2.v >COQDEP theories/Sets/Image.v >COQDEP theories/Sets/Relations_1_facts.v >COQDEP theories/Sets/Finite_sets_facts.v >COQDEP theories/Sets/Relations_1.v >COQDEP theories/Sets/Finite_sets.v >COQDEP theories/Sets/Powerset_facts.v >COQDEP theories/Sets/Ensembles.v >COQDEP theories/Sets/Powerset_Classical_facts.v >COQDEP theories/Sets/Cpo.v >COQDEP theories/Sets/Powerset.v >COQDEP theories/Sets/Constructive_sets.v >COQDEP theories/Sets/Permut.v >COQDEP theories/Sets/Classical_sets.v >COQDEP theories/Strings/String.v >COQDEP theories/Strings/Ascii.v >COQDEP theories/Lists/ListTactics.v >COQDEP theories/Lists/SetoidList.v >COQDEP theories/Lists/List.v >COQDEP theories/Lists/TheoryList.v >COQDEP theories/Lists/StreamMemo.v >COQDEP theories/Lists/Streams.v >COQDEP theories/Lists/ListSet.v >COQDEP theories/Lists/MonoList.v >COQDEP theories/Setoids/Setoid.v >COQDEP theories/ZArith/Zgcd_alt.v >COQDEP theories/ZArith/ZOdiv.v >COQDEP theories/ZArith/ZOdiv_def.v >COQDEP theories/ZArith/Zpow_facts.v >COQDEP theories/ZArith/Zpow_def.v >COQDEP theories/ZArith/Int.v >COQDEP theories/ZArith/Znumtheory.v >COQDEP theories/ZArith/Zbinary.v >COQDEP theories/ZArith/Zbool.v >COQDEP theories/ZArith/ZArith_base.v >COQDEP theories/ZArith/Zwf.v >COQDEP theories/ZArith/Zsqrt.v >COQDEP theories/ZArith/Zdiv.v >COQDEP theories/ZArith/Zcomplements.v >COQDEP theories/ZArith/Zpower.v >COQDEP theories/ZArith/Zlogarithm.v >COQDEP theories/ZArith/Zhints.v >COQDEP theories/ZArith/Zeven.v >COQDEP theories/ZArith/Zminmax.v >COQDEP theories/ZArith/Zmax.v >COQDEP theories/ZArith/Zmin.v >COQDEP theories/ZArith/Zabs.v >COQDEP theories/ZArith/Zorder.v >COQDEP theories/ZArith/Znat.v >COQDEP theories/ZArith/Zcompare.v >COQDEP theories/ZArith/Zmisc.v >COQDEP theories/ZArith/auxiliary.v >COQDEP theories/ZArith/ZArith_dec.v >COQDEP theories/ZArith/ZArith.v >COQDEP theories/ZArith/Wf_Z.v >COQDEP theories/ZArith/BinInt.v >COQDEP theories/NArith/Ndist.v >COQDEP theories/NArith/Ndec.v >COQDEP theories/NArith/Ndigits.v >COQDEP theories/NArith/Nnat.v >COQDEP theories/NArith/NArith.v >COQDEP theories/NArith/BinNat.v >COQDEP theories/NArith/Pnat.v >COQDEP theories/NArith/BinPos.v >COQDEP theories/Bool/Bvector.v >COQDEP theories/Bool/BoolEq.v >COQDEP theories/Bool/Sumbool.v >COQDEP theories/Bool/DecBool.v >COQDEP theories/Bool/Zerob.v >COQDEP theories/Bool/IfProp.v >COQDEP theories/Bool/Bool.v >COQDEP theories/Arith/Arith_base.v >COQDEP theories/Arith/Factorial.v >COQDEP theories/Arith/Bool_nat.v >COQDEP theories/Arith/Max.v >COQDEP theories/Arith/Wf_nat.v >COQDEP theories/Arith/Plus.v >COQDEP theories/Arith/Euclid.v >COQDEP theories/Arith/Peano_dec.v >COQDEP theories/Arith/EqNat.v >COQDEP theories/Arith/Even.v >COQDEP theories/Arith/Mult.v >COQDEP theories/Arith/Minus.v >COQDEP theories/Arith/Div2.v >COQDEP theories/Arith/Min.v >COQDEP theories/Arith/Compare_dec.v >COQDEP theories/Arith/Lt.v >COQDEP theories/Arith/Compare.v >COQDEP theories/Arith/Le.v >COQDEP theories/Arith/Between.v >COQDEP theories/Arith/Gt.v >COQDEP theories/Arith/Arith.v >COQDEP theories/Logic/FunctionalExtensionality.v >COQDEP theories/Logic/SetIsType.v >COQDEP theories/Logic/IndefiniteDescription.v >COQDEP theories/Logic/Description.v >COQDEP theories/Logic/ConstructiveEpsilon.v >COQDEP theories/Logic/Epsilon.v >COQDEP theories/Logic/DecidableTypeEx.v >COQDEP theories/Logic/DecidableType.v >COQDEP theories/Logic/ClassicalUniqueChoice.v >COQDEP theories/Logic/ClassicalEpsilon.v >COQDEP theories/Logic/ProofIrrelevanceFacts.v >COQDEP theories/Logic/EqdepFacts.v >COQDEP theories/Logic/Diaconescu.v >COQDEP theories/Logic/RelationalChoice.v >COQDEP theories/Logic/ClassicalDescription.v >COQDEP theories/Logic/ClassicalChoice.v >COQDEP theories/Logic/JMeq.v >COQDEP theories/Logic/Decidable.v >COQDEP theories/Logic/Eqdep_dec.v >COQDEP theories/Logic/Berardi.v >COQDEP theories/Logic/ChoiceFacts.v >COQDEP theories/Logic/ClassicalFacts.v >COQDEP theories/Logic/Classical_Pred_Type.v >COQDEP theories/Logic/Classical_Prop.v >COQDEP theories/Logic/Eqdep.v >COQDEP theories/Logic/Classical_Pred_Set.v >COQDEP theories/Logic/Classical_Type.v >COQDEP theories/Logic/Classical.v >COQDEP theories/Logic/ProofIrrelevance.v >COQDEP theories/Logic/Hurkens.v >COQDEP theories/Init/Prelude.v >COQDEP theories/Init/Tactics.v >COQDEP theories/Init/Wf.v >COQDEP theories/Init/Logic_Type.v >COQDEP theories/Init/Specif.v >COQDEP theories/Init/Logic.v >COQDEP theories/Init/Peano.v >COQDEP theories/Init/Datatypes.v >COQDEP theories/Init/Notations.v >make[1]: Leaving directory `/var/tmp/portage/sci-mathematics/coq-8.2_p1-r1/work/coq-8.2pl1' >make[1]: Entering directory `/var/tmp/portage/sci-mathematics/coq-8.2_p1-r1/work/coq-8.2pl1' >CHECK revision >OCAMLOPT scripts/tolink.ml >OCAMLOPT scripts/coqmktop.ml >OCAMLOPT -o bin/coqmktop.opt >true bin/coqmktop.opt >cd bin; ln -sf coqmktop.opt coqmktop >OCAMLOPT lib/bigint.ml >OCAMLOPT lib/hashcons.ml >OCAMLOPT lib/dyn.ml >OCAMLC lib/bstack.mli >OCAMLOPT lib/bstack.ml >OCAMLC lib/edit.mli >OCAMLOPT lib/edit.ml >OCAMLC lib/gset.mli >OCAMLOPT lib/gset.ml >OCAMLC lib/gmap.mli >OCAMLOPT lib/gmap.ml >OCAMLC lib/tlm.mli >OCAMLOPT lib/tlm.ml >OCAMLC lib/gmapl.mli >OCAMLOPT lib/gmapl.ml >OCAMLC lib/profile.mli >OCAMLOPT lib/profile.ml >OCAMLC lib/explore.mli >OCAMLOPT lib/explore.ml >OCAMLOPT lib/predicate.ml >OCAMLOPT lib/rtree.ml >OCAMLC lib/heap.mli >OCAMLOPT lib/heap.ml >OCAMLOPT lib/option.ml >OCAMLOPT -a -o lib/lib.cmxa >OCAMLOPT kernel/names.ml >OCAMLOPT kernel/univ.ml >OCAMLOPT kernel/esubst.ml >OCAMLOPT -rectypes kernel/term.ml >OCAMLOPT kernel/mod_subst.ml >OCAMLOPT kernel/sign.ml >OCAMLOPT kernel/cbytecodes.ml >OCAMLOPT kernel/copcodes.ml >OCAMLOPT kernel/cemitcodes.ml >OCAMLOPT kernel/conv_oracle.ml >OCAMLC kernel/vm.mli >OCAMLOPT kernel/vm.ml >OCAMLOPT kernel/retroknowledge.ml >OCAMLOPT kernel/declarations.ml >OCAMLOPT kernel/pre_env.ml >OCAMLOPT kernel/cbytegen.ml >OCAMLOPT kernel/environ.ml >OCAMLC kernel/csymtable.mli >OCAMLOPT kernel/csymtable.ml >OCAMLOPT kernel/closure.ml >OCAMLOPT kernel/reduction.ml >OCAMLOPT kernel/type_errors.ml >OCAMLOPT kernel/entries.ml >OCAMLOPT kernel/modops.ml >OCAMLOPT kernel/inductive.ml >OCAMLC kernel/vconv.mli >OCAMLOPT kernel/vconv.ml >OCAMLOPT kernel/typeops.ml >OCAMLOPT kernel/indtypes.ml >OCAMLOPT kernel/cooking.ml >OCAMLOPT kernel/term_typing.ml >OCAMLOPT kernel/subtyping.ml >OCAMLOPT kernel/mod_typing.ml >OCAMLOPT kernel/safe_typing.ml >OCAMLOPT -a -o kernel/kernel.cmxa >OCAMLOPT library/nameops.ml >OCAMLOPT library/libnames.ml >OCAMLOPT library/libobject.ml >OCAMLOPT library/summary.ml >OCAMLOPT -rectypes library/nametab.ml >OCAMLOPT library/global.ml >OCAMLOPT library/lib.ml >OCAMLC library/declaremods.mli >OCAMLOPT library/declaremods.ml >OCAMLC library/library.mli >OCAMLOPT library/library.ml >OCAMLC library/states.mli >OCAMLOPT library/states.ml >OCAMLOPT library/decl_kinds.ml >OCAMLC library/dischargedhypsmap.mli >OCAMLOPT library/dischargedhypsmap.ml >OCAMLOPT library/goptions.ml >OCAMLC library/decls.mli >OCAMLOPT library/decls.ml >OCAMLC library/heads.mli >OCAMLOPT library/heads.ml >OCAMLOPT -a -o library/library.cmxa >OCAMLOPT pretyping/termops.ml >OCAMLOPT pretyping/evd.ml >OCAMLOPT pretyping/reductionops.ml >OCAMLC pretyping/vnorm.mli >OCAMLOPT pretyping/vnorm.ml >OCAMLOPT pretyping/inductiveops.ml >OCAMLC pretyping/retyping.mli >OCAMLOPT pretyping/retyping.ml >OCAMLC pretyping/cbv.mli >OCAMLOPT pretyping/cbv.ml >OCAMLOPT pretyping/rawterm.ml >OCAMLC pretyping/pretype_errors.mli >OCAMLOPT pretyping/pretype_errors.ml >OCAMLC pretyping/typing.mli >OCAMLOPT pretyping/typing.ml >OCAMLC pretyping/tacred.mli >OCAMLOPT pretyping/tacred.ml >OCAMLOPT pretyping/classops.ml >OCAMLC pretyping/recordops.mli >OCAMLOPT pretyping/recordops.ml >OCAMLC pretyping/evarutil.mli >OCAMLOPT pretyping/evarutil.ml >OCAMLC pretyping/evarconv.mli >OCAMLOPT pretyping/evarconv.ml >OCAMLOPT pretyping/detyping.ml >OCAMLOPT interp/topconstr.ml >OCAMLC pretyping/typeclasses_errors.mli >OCAMLOPT pretyping/typeclasses_errors.ml >OCAMLC pretyping/typeclasses.mli >OCAMLOPT pretyping/typeclasses.ml >OCAMLC pretyping/coercion.mli >OCAMLOPT pretyping/coercion.ml >OCAMLOPT pretyping/pattern.ml >OCAMLC pretyping/unification.mli >OCAMLOPT pretyping/unification.ml >OCAMLC pretyping/clenv.mli >OCAMLOPT pretyping/clenv.ml >OCAMLC pretyping/indrec.mli >OCAMLOPT pretyping/indrec.ml >OCAMLC pretyping/cases.mli >OCAMLOPT pretyping/cases.ml >OCAMLC pretyping/pretyping.mli >OCAMLOPT pretyping/pretyping.ml >OCAMLC pretyping/matching.mli >OCAMLOPT pretyping/matching.ml >OCAMLOPT -a -o pretyping/pretyping.cmxa >OCAMLOPT4 parsing/lexer.ml4 >OCAMLOPT interp/ppextend.ml >OCAMLOPT interp/notation.ml >OCAMLC interp/dumpglob.mli >OCAMLOPT interp/dumpglob.ml >OCAMLOPT interp/genarg.ml >OCAMLC interp/syntax_def.mli >OCAMLOPT interp/syntax_def.ml >OCAMLC interp/reserve.mli >OCAMLOPT interp/reserve.ml >OCAMLC library/impargs.mli >OCAMLOPT library/impargs.ml >OCAMLC interp/implicit_quantifiers.mli >OCAMLOPT interp/implicit_quantifiers.ml >OCAMLC interp/constrintern.mli >OCAMLOPT interp/constrintern.ml >OCAMLC interp/modintern.mli >OCAMLOPT interp/modintern.ml >OCAMLC interp/constrextern.mli >OCAMLOPT interp/constrextern.ml >OCAMLC interp/coqlib.mli >OCAMLOPT interp/coqlib.ml >OCAMLC toplevel/discharge.mli >OCAMLOPT toplevel/discharge.ml >OCAMLC library/declare.mli >OCAMLOPT library/declare.ml >OCAMLOPT -a -o interp/interp.cmxa >OCAMLOPT -rectypes proofs/tacexpr.ml >OCAMLC proofs/proof_type.mli >OCAMLOPT proofs/proof_type.ml >OCAMLC proofs/redexpr.mli >OCAMLOPT proofs/redexpr.ml >OCAMLC proofs/proof_trees.mli >OCAMLOPT proofs/proof_trees.ml >OCAMLC proofs/logic.mli >OCAMLOPT proofs/logic.ml >OCAMLC proofs/refiner.mli >OCAMLOPT proofs/refiner.ml >OCAMLC proofs/evar_refiner.mli >OCAMLOPT proofs/evar_refiner.ml >OCAMLC proofs/tacmach.mli >OCAMLOPT proofs/tacmach.ml >OCAMLC proofs/pfedit.mli >OCAMLOPT proofs/pfedit.ml >OCAMLC proofs/tactic_debug.mli >OCAMLOPT proofs/tactic_debug.ml >OCAMLC proofs/clenvtac.mli >OCAMLOPT proofs/clenvtac.ml >OCAMLC proofs/decl_mode.mli >OCAMLOPT proofs/decl_mode.ml >OCAMLOPT -a -o proofs/proofs.cmxa >OCAMLOPT parsing/extend.ml >OCAMLOPT4 parsing/pcoq.ml4 >OCAMLOPT toplevel/vernacexpr.ml >OCAMLC parsing/egrammar.mli >OCAMLOPT parsing/egrammar.ml >OCAMLOPT4 parsing/g_xml.ml4 >OCAMLC parsing/ppconstr.mli >OCAMLOPT parsing/ppconstr.ml >OCAMLC parsing/printer.mli >OCAMLOPT parsing/printer.ml >OCAMLC parsing/pptactic.mli >OCAMLOPT -rectypes parsing/pptactic.ml >OCAMLC parsing/ppdecl_proof.mli >OCAMLOPT parsing/ppdecl_proof.ml >OCAMLC parsing/tactic_printer.mli >OCAMLOPT parsing/tactic_printer.ml >OCAMLC parsing/printmod.mli >OCAMLOPT parsing/printmod.ml >OCAMLC parsing/prettyp.mli >OCAMLOPT parsing/prettyp.ml >OCAMLC parsing/search.mli >OCAMLOPT parsing/search.ml >OCAMLOPT -a -o parsing/parsing.cmxa >OCAMLC tactics/dn.mli >OCAMLOPT tactics/dn.ml >OCAMLC tactics/termdn.mli >OCAMLOPT tactics/termdn.ml >OCAMLC tactics/btermdn.mli >OCAMLOPT tactics/btermdn.ml >OCAMLC tactics/nbtermdn.mli >OCAMLOPT tactics/nbtermdn.ml >OCAMLC tactics/tacticals.mli >OCAMLOPT tactics/tacticals.ml >OCAMLC tactics/hipattern.mli >OCAMLOPT4 tactics/hipattern.ml4 >OCAMLC tactics/tactics.mli >OCAMLOPT tactics/tactics.ml >OCAMLC tactics/hiddentac.mli >OCAMLOPT tactics/hiddentac.ml >OCAMLC tactics/elim.mli >OCAMLOPT tactics/elim.ml >OCAMLC tactics/dhyp.mli >OCAMLOPT tactics/dhyp.ml >OCAMLC tactics/auto.mli >OCAMLOPT tactics/auto.ml >OCAMLC toplevel/ind_tables.mli >OCAMLOPT toplevel/ind_tables.ml >OCAMLC tactics/equality.mli >OCAMLOPT tactics/equality.ml >OCAMLC tactics/contradiction.mli >OCAMLOPT tactics/contradiction.ml >OCAMLC tactics/inv.mli >OCAMLOPT tactics/inv.ml >OCAMLC tactics/leminv.mli >OCAMLOPT tactics/leminv.ml >OCAMLC tactics/tacinterp.mli >OCAMLOPT tactics/tacinterp.ml >OCAMLC toplevel/himsg.mli >OCAMLOPT toplevel/himsg.ml >OCAMLC toplevel/vernacinterp.mli >OCAMLOPT toplevel/vernacinterp.ml >OCAMLC tactics/autorewrite.mli >OCAMLOPT tactics/autorewrite.ml >OCAMLC tactics/evar_tactics.mli >OCAMLOPT tactics/evar_tactics.ml >OCAMLC tactics/decl_interp.mli >OCAMLOPT tactics/decl_interp.ml >OCAMLC tactics/decl_proof_instr.mli >OCAMLOPT tactics/decl_proof_instr.ml >OCAMLOPT -a -o tactics/tactics.cmxa >OCAMLC toplevel/cerrors.mli >OCAMLOPT toplevel/cerrors.ml >OCAMLC toplevel/class.mli >OCAMLOPT toplevel/class.ml >OCAMLC toplevel/metasyntax.mli >OCAMLOPT toplevel/metasyntax.ml >OCAMLC toplevel/auto_ind_decl.mli >OCAMLOPT toplevel/auto_ind_decl.ml >OCAMLC toplevel/command.mli >OCAMLOPT toplevel/command.ml >OCAMLC toplevel/record.mli >OCAMLOPT toplevel/record.ml >OCAMLC parsing/ppvernac.mli >OCAMLOPT parsing/ppvernac.ml >OCAMLC toplevel/classes.mli >OCAMLOPT toplevel/classes.ml >CAMLP4O toplevel/mltop.ml4 >OCAMLC toplevel/mltop.mli >OCAMLOPT toplevel/mltop.optml >OCAMLC toplevel/vernacentries.mli >OCAMLOPT toplevel/vernacentries.ml >OCAMLC toplevel/whelp.mli >OCAMLOPT4 toplevel/whelp.ml4 >OCAMLC toplevel/vernac.mli >OCAMLOPT toplevel/vernac.ml >OCAMLC toplevel/line_oriented_parser.mli >OCAMLOPT toplevel/line_oriented_parser.ml >OCAMLC toplevel/protectedtoplevel.mli >OCAMLOPT toplevel/protectedtoplevel.ml >OCAMLC toplevel/toplevel.mli >OCAMLOPT toplevel/toplevel.ml >OCAMLC toplevel/usage.mli >OCAMLOPT toplevel/usage.ml >OCAMLC toplevel/coqinit.mli >OCAMLOPT toplevel/coqinit.ml >OCAMLC toplevel/coqtop.mli >OCAMLOPT toplevel/coqtop.ml >OCAMLOPT -a -o toplevel/toplevel.cmxa >OCAMLOPT4 parsing/g_constr.ml4 >OCAMLOPT4 parsing/g_vernac.ml4 >OCAMLOPT4 parsing/g_prim.ml4 >OCAMLOPT4 parsing/g_proofs.ml4 >OCAMLOPT4 parsing/g_tactic.ml4 >OCAMLOPT4 parsing/g_ltac.ml4 >OCAMLC parsing/g_natsyntax.mli >OCAMLOPT parsing/g_natsyntax.ml >OCAMLC parsing/g_zsyntax.mli >OCAMLOPT parsing/g_zsyntax.ml >OCAMLOPT parsing/g_rsyntax.ml >OCAMLOPT parsing/g_ascii_syntax.ml >OCAMLOPT parsing/g_string_syntax.ml >OCAMLOPT4 parsing/g_decl_mode.ml4 >OCAMLC parsing/g_intsyntax.mli >OCAMLOPT parsing/g_intsyntax.ml >OCAMLOPT -a -o parsing/highparsing.cmxa >OCAMLC tactics/refine.mli >OCAMLOPT tactics/refine.ml >OCAMLC tactics/extraargs.mli >OCAMLOPT4 tactics/extraargs.ml4 >OCAMLC tactics/extratactics.mli >OCAMLOPT4 tactics/extratactics.ml4 >OCAMLC tactics/eauto.mli >OCAMLOPT4 tactics/eauto.ml4 >OCAMLOPT4 tactics/class_tactics.ml4 >OCAMLOPT4 tactics/tauto.ml4 >OCAMLOPT4 tactics/eqdecide.ml4 >OCAMLOPT -a -o tactics/hightactics.cmxa >OCAMLOPT contrib/omega/omega.ml >OCAMLOPT contrib/omega/coq_omega.ml >OCAMLOPT4 contrib/omega/g_omega.ml4 >OCAMLC contrib/romega/const_omega.mli >OCAMLOPT contrib/romega/const_omega.ml >OCAMLOPT contrib/romega/refl_omega.ml >OCAMLOPT4 contrib/romega/g_romega.ml4 >OCAMLC contrib/micromega/micromega.mli >OCAMLOPT contrib/micromega/micromega.ml >OCAMLOPT contrib/micromega/mutils.ml >OCAMLOPT contrib/micromega/vector.ml >OCAMLOPT contrib/micromega/mfourier.ml >OCAMLC contrib/micromega/sos.mli >OCAMLOPT contrib/micromega/sos.ml >OCAMLOPT contrib/micromega/certificate.ml >OCAMLOPT contrib/micromega/coq_micromega.ml >OCAMLOPT contrib/ring/quote.ml >OCAMLOPT contrib/ring/ring.ml >OCAMLOPT4 contrib/micromega/g_micromega.ml4 >OCAMLOPT4 contrib/ring/g_quote.ml4 >OCAMLOPT4 contrib/ring/g_ring.ml4 >OCAMLOPT4 contrib/setoid_ring/newring.ml4 >OCAMLC contrib/dp/fol.mli >OCAMLC contrib/dp/dp_why.mli >OCAMLOPT contrib/dp/dp_why.ml >OCAMLC contrib/dp/dp_zenon.mli >OCAMLOPT contrib/dp/dp_zenon.ml >OCAMLC contrib/dp/dp.mli >OCAMLOPT contrib/dp/dp.ml >OCAMLOPT contrib/dp/dp_gappa.ml >OCAMLOPT4 contrib/dp/g_dp.ml4 >OCAMLOPT4 contrib/field/field.ml4 >OCAMLOPT contrib/fourier/fourier.ml >OCAMLOPT contrib/fourier/fourierR.ml >OCAMLOPT4 contrib/fourier/g_fourier.ml4 >OCAMLC contrib/extraction/miniml.mli >OCAMLC contrib/extraction/table.mli >OCAMLOPT contrib/extraction/table.ml >OCAMLC contrib/extraction/mlutil.mli >OCAMLOPT contrib/extraction/mlutil.ml >OCAMLC contrib/extraction/modutil.mli >OCAMLOPT contrib/extraction/modutil.ml >OCAMLC contrib/extraction/extraction.mli >OCAMLOPT contrib/extraction/extraction.ml >OCAMLC contrib/extraction/common.mli >OCAMLOPT contrib/extraction/common.ml >OCAMLC contrib/extraction/ocaml.mli >OCAMLOPT contrib/extraction/ocaml.ml >OCAMLC contrib/extraction/haskell.mli >OCAMLOPT contrib/extraction/haskell.ml >OCAMLC contrib/extraction/scheme.mli >OCAMLOPT contrib/extraction/scheme.ml >OCAMLC contrib/extraction/extract_env.mli >OCAMLOPT contrib/extraction/extract_env.ml >OCAMLOPT4 contrib/extraction/g_extraction.ml4 >OCAMLC contrib/xml/unshare.mli >OCAMLOPT contrib/xml/unshare.ml >OCAMLC contrib/xml/xml.mli >OCAMLOPT4 contrib/xml/xml.ml4 >OCAMLOPT contrib/xml/acic.ml >OCAMLC contrib/xml/acic.ml >OCAMLC contrib/xml/doubleTypeInference.mli >OCAMLOPT contrib/xml/doubleTypeInference.ml >OCAMLOPT contrib/xml/cic2acic.ml >OCAMLOPT4 contrib/xml/acic2Xml.ml4 >OCAMLOPT contrib/xml/proof2aproof.ml >OCAMLC contrib/xml/proof2aproof.ml >OCAMLC contrib/xml/xmlcommand.mli >OCAMLOPT contrib/xml/xmlcommand.ml >OCAMLOPT4 contrib/xml/proofTree2Xml.ml4 >OCAMLOPT4 contrib/xml/xmlentries.ml4 >OCAMLOPT contrib/xml/cic2Xml.ml >OCAMLOPT4 contrib/xml/dumptree.ml4 >OCAMLC contrib/cc/ccalgo.mli >OCAMLOPT contrib/cc/ccalgo.ml >OCAMLC contrib/cc/ccproof.mli >OCAMLOPT contrib/cc/ccproof.ml >OCAMLC contrib/cc/cctac.mli >OCAMLOPT contrib/cc/cctac.ml >OCAMLOPT4 contrib/cc/g_congruence.ml4 >OCAMLC contrib/firstorder/formula.mli >OCAMLOPT contrib/firstorder/formula.ml >OCAMLC contrib/firstorder/unify.mli >OCAMLOPT contrib/firstorder/unify.ml >OCAMLC contrib/firstorder/sequent.mli >OCAMLOPT contrib/firstorder/sequent.ml >OCAMLC contrib/firstorder/rules.mli >OCAMLOPT contrib/firstorder/rules.ml >OCAMLC contrib/firstorder/instances.mli >OCAMLOPT contrib/firstorder/instances.ml >OCAMLC contrib/firstorder/ground.mli >OCAMLOPT contrib/firstorder/ground.ml >OCAMLOPT4 contrib/firstorder/g_ground.ml4 >OCAMLC contrib/subtac/subtac_utils.mli >OCAMLOPT contrib/subtac/subtac_utils.ml >OCAMLC contrib/subtac/eterm.mli >OCAMLOPT contrib/subtac/eterm.ml >OCAMLOPT4 contrib/subtac/g_eterm.ml4 >OCAMLC contrib/subtac/subtac_errors.mli >OCAMLOPT contrib/subtac/subtac_errors.ml >OCAMLC contrib/subtac/subtac_coercion.mli >OCAMLOPT contrib/subtac/subtac_coercion.ml >OCAMLC contrib/subtac/subtac_obligations.mli >OCAMLOPT contrib/subtac/subtac_obligations.ml >OCAMLC contrib/subtac/subtac_cases.mli >OCAMLOPT contrib/subtac/subtac_cases.ml >OCAMLOPT contrib/subtac/subtac_pretyping_F.ml >OCAMLC contrib/subtac/subtac_pretyping.mli >OCAMLOPT contrib/subtac/subtac_pretyping.ml >OCAMLC contrib/subtac/subtac_command.mli >OCAMLOPT contrib/subtac/subtac_command.ml >OCAMLC contrib/subtac/subtac_classes.mli >OCAMLOPT contrib/subtac/subtac_classes.ml >OCAMLC contrib/subtac/subtac.mli >OCAMLOPT contrib/subtac/subtac.ml >OCAMLOPT4 contrib/subtac/g_subtac.ml4 >OCAMLOPT4 contrib/subtac/equations.ml4 >OCAMLC contrib/rtauto/proof_search.mli >OCAMLOPT contrib/rtauto/proof_search.ml >OCAMLC contrib/rtauto/refl_tauto.mli >OCAMLOPT contrib/rtauto/refl_tauto.ml >OCAMLOPT4 contrib/rtauto/g_rtauto.ml4 >OCAMLC contrib/funind/indfun_common.mli >OCAMLOPT contrib/funind/indfun_common.ml >OCAMLC contrib/funind/rawtermops.mli >OCAMLOPT contrib/funind/rawtermops.ml >OCAMLOPT contrib/funind/recdef.ml >OCAMLC contrib/funind/rawterm_to_relation.mli >OCAMLOPT contrib/funind/rawterm_to_relation.ml >OCAMLC contrib/funind/functional_principles_proofs.mli >OCAMLOPT contrib/funind/functional_principles_proofs.ml >OCAMLC contrib/funind/functional_principles_types.mli >OCAMLOPT contrib/funind/functional_principles_types.ml >OCAMLOPT contrib/funind/invfun.ml >OCAMLOPT contrib/funind/indfun.ml >OCAMLOPT contrib/funind/merge.ml >OCAMLOPT4 contrib/funind/g_indfun.ml4 >OCAMLOPT -a -o contrib/contrib.cmxa >OCAMLC kernel/byterun/coq_fix_code.c >OCAMLC kernel/byterun/coq_memory.c >OCAMLC kernel/byterun/coq_values.c >OCAMLC kernel/byterun/coq_interp.c >cd kernel/byterun/ && \ > "ocamlmklib" -oc coqrun coq_fix_code.o coq_memory.o coq_values.o coq_interp.o >"ranlib" kernel/byterun/libcoqrun.a >COQMKTOP -o bin/coqtop.opt >true bin/coqtop.opt >COQC -nois theories/Init/Notations.v >COQC -nois theories/Init/Logic.v >Defining 'IF' as keyword >Defining 'exists2' as keyword >COQC -nois theories/Init/Datatypes.v >COQC -nois theories/Init/Peano.v >COQC -nois theories/Init/Specif.v >COQC -nois theories/Init/Logic_Type.v >COQC -nois theories/Init/Wf.v >COQC -nois theories/Init/Tactics.v >COQC -nois theories/Init/Prelude.v >COQDEP states/MakeInitial.v >BUILD states/initial.coq >COQC theories/Logic/Hurkens.v >COQC theories/Logic/EqdepFacts.v >COQC theories/Logic/ProofIrrelevanceFacts.v >COQC theories/Logic/ProofIrrelevance.v >COQC theories/Logic/ClassicalFacts.v >COQC theories/Logic/Classical_Prop.v >COQC theories/Logic/Classical_Pred_Type.v >COQC theories/Logic/Classical.v >COQC theories/Logic/Classical_Type.v >COQC theories/Logic/Classical_Pred_Set.v >COQC theories/Logic/Eqdep.v >COQC theories/Arith/Le.v >COQC theories/Arith/Lt.v >COQC theories/Arith/Plus.v >COQC theories/Arith/Gt.v >COQC theories/Logic/Decidable.v >COQC theories/Arith/Compare_dec.v >COQC theories/Arith/Wf_nat.v >COQC theories/Program/Basics.v >COQC theories/Program/Tactics.v >COQC theories/Relations/Relation_Definitions.v >COQC theories/Classes/Init.v >COQC theories/Arith/Minus.v >COQC theories/Arith/Min.v >COQC theories/Bool/Bool.v >COQC theories/Lists/List.v >COQC theories/Classes/RelationClasses.v >COQC theories/Classes/Morphisms.v >COQC theories/Classes/Morphisms_Prop.v >COQC theories/Classes/Equivalence.v >COQC theories/Classes/SetoidTactics.v >COQC theories/Setoids/Setoid.v >COQC theories/Logic/ChoiceFacts.v >COQC theories/Logic/Berardi.v >COQC theories/Logic/Eqdep_dec.v >COQC theories/Logic/JMeq.v >COQC theories/Logic/ClassicalUniqueChoice.v >COQC theories/Logic/RelationalChoice.v >COQC theories/Logic/ClassicalChoice.v >COQC theories/Logic/ClassicalDescription.v >COQC theories/Logic/Diaconescu.v >COQC theories/Logic/ClassicalEpsilon.v >COQC theories/Sets/Permut.v >COQC theories/Sets/Multiset.v >COQC theories/Relations/Relation_Operators.v >COQC theories/Relations/Operators_Properties.v >COQC theories/Relations/Relations.v >COQC theories/Arith/Mult.v >COQC theories/Arith/Between.v >COQC theories/Arith/Peano_dec.v >COQC theories/Arith/Factorial.v >COQC theories/Arith/EqNat.v >COQC theories/Arith/Arith_base.v >COQC theories/NArith/BinPos.v >COQC theories/NArith/BinNat.v >COQC theories/Bool/Sumbool.v >COQC theories/Arith/Even.v >COQC theories/Arith/Div2.v >COQC theories/Arith/Max.v >COQC theories/NArith/Pnat.v >COQC theories/ZArith/BinInt.v >COQC theories/ZArith/Zcompare.v >COQC theories/ZArith/Zorder.v >COQC theories/ZArith/Zmax.v >COQC theories/ZArith/Zmin.v >COQC theories/ZArith/Znat.v >COQC theories/NArith/Nnat.v >COQC contrib/setoid_ring/Ring_theory.v >COQC theories/Lists/ListTactics.v >COQC contrib/setoid_ring/BinList.v >COQC contrib/setoid_ring/Ring_polynom.v >COQC theories/ZArith/Zeven.v >COQC theories/ZArith/Zminmax.v >COQC theories/ZArith/ZArith_dec.v >COQC theories/ZArith/Zabs.v >COQC theories/ZArith/auxiliary.v >COQC theories/ZArith/Zbool.v >COQC theories/ZArith/Zmisc.v >COQC theories/ZArith/Wf_Z.v >COQC theories/ZArith/Zhints.v >COQC theories/ZArith/ZArith_base.v >COQC theories/ZArith/Zpow_def.v >COQC theories/ZArith/ZOdiv_def.v >COQC contrib/setoid_ring/InitialRing.v >COQC contrib/setoid_ring/Ring_tac.v >COQC contrib/setoid_ring/Ring_base.v >COQC contrib/setoid_ring/Ring.v >COQC contrib/setoid_ring/ArithRing.v >COQC theories/Arith/Arith.v >COQC theories/Sorting/Permutation.v >COQC theories/Sorting/Sorting.v >COQC theories/Lists/SetoidList.v >COQC theories/Logic/DecidableType.v >COQC theories/FSets/OrderedType.v >COQC contrib/setoid_ring/ZArithRing.v >COQC contrib/omega/OmegaLemmas.v >COQC theories/Bool/Bvector.v >COQC theories/NArith/Ndigits.v >COQC contrib/setoid_ring/NArithRing.v >COQC theories/NArith/NArith.v >COQC contrib/omega/PreOmega.v >COQC contrib/omega/Omega.v >COQC theories/ZArith/Zcomplements.v >COQC theories/ZArith/Zsqrt.v >COQC theories/ZArith/Zpower.v >COQC theories/ZArith/Zdiv.v >Defining 'mod' as keyword >COQC theories/ZArith/Zlogarithm.v >COQC theories/ZArith/ZArith.v >COQC theories/NArith/Ndec.v >COQC theories/FSets/OrderedTypeEx.v >COQC theories/Logic/DecidableTypeEx.v >COQC theories/Logic/Epsilon.v >COQC theories/Logic/ConstructiveEpsilon.v >COQC theories/Logic/Description.v >COQC theories/Logic/IndefiniteDescription.v >COQC theories/Logic/SetIsType.v >COQC theories/Logic/FunctionalExtensionality.v >COQC theories/Arith/Compare.v >COQC theories/Arith/Euclid.v >COQC theories/Arith/Bool_nat.v >COQC theories/Bool/IfProp.v >COQC theories/Bool/Zerob.v >COQC theories/Bool/DecBool.v >COQC theories/Bool/BoolEq.v >COQC theories/NArith/Ndist.v >COQC theories/ZArith/Zwf.v >COQC theories/ZArith/Zbinary.v >COQC theories/ZArith/Znumtheory.v >COQC contrib/romega/ReflOmegaCore.v >COQC contrib/romega/ROmega.v >COQC theories/ZArith/Int.v >COQC theories/ZArith/Zpow_facts.v >COQC theories/ZArith/ZOdiv.v >Defining 'mod' as keyword >COQC theories/ZArith/Zgcd_alt.v >COQC theories/Lists/MonoList.v >COQC theories/Lists/ListSet.v >COQC theories/Lists/Streams.v >COQC theories/Lists/StreamMemo.v >COQC theories/Lists/TheoryList.v >COQC theories/Strings/Ascii.v >COQC theories/Strings/String.v >COQC theories/Sets/Ensembles.v >COQC theories/Sets/Constructive_sets.v >COQC theories/Sets/Classical_sets.v >COQC theories/Sets/Relations_1.v >COQC theories/Sets/Relations_1_facts.v >COQC theories/Sets/Partial_Order.v >COQC theories/Sets/Cpo.v >COQC theories/Sets/Powerset.v >COQC theories/Sets/Powerset_facts.v >COQC theories/Sets/Powerset_Classical_facts.v >COQC theories/Sets/Finite_sets.v >COQC theories/Sets/Finite_sets_facts.v >COQC theories/Sets/Image.v >COQC theories/Sets/Relations_2.v >COQC theories/Sets/Infinite_sets.v >COQC theories/Sets/Relations_2_facts.v >COQC theories/Sets/Integers.v >COQC theories/Sets/Relations_3.v >COQC theories/Sets/Relations_3_facts.v >COQC theories/Sets/Uniset.v >COQC theories/FSets/OrderedTypeAlt.v >COQC theories/FSets/FSetInterface.v >COQC theories/FSets/FSetList.v >COQC theories/FSets/FSetBridge.v >COQC theories/FSets/FSetFacts.v >COQC theories/FSets/FSetDecide.v >COQC theories/FSets/FSetProperties.v >COQC theories/FSets/FSetEqProperties.v >COQC theories/FSets/FSetWeakList.v >COQC theories/FSets/FSetAVL.v >COQC theories/FSets/FSets.v >COQC theories/FSets/FMapInterface.v >COQC theories/FSets/FMapList.v >COQC theories/FSets/FMapFacts.v >COQC theories/FSets/FMapWeakList.v >COQC theories/FSets/FMapPositive.v >COQC theories/FSets/FSetToFiniteSet.v >COQC theories/FSets/FMaps.v >COQC contrib/funind/Recdef.v >COQC theories/FSets/FSetFullAVL.v >COQC theories/FSets/FMapAVL.v >COQC theories/FSets/FMapFullAVL.v >COQC theories/Wellfounded/Disjoint_Union.v >COQC theories/Wellfounded/Inclusion.v >COQC theories/Wellfounded/Inverse_Image.v >COQC theories/Wellfounded/Transitive_Closure.v >COQC theories/Wellfounded/Union.v >COQC theories/Wellfounded/Lexicographic_Exponentiation.v >COQC theories/Wellfounded/Lexicographic_Product.v >COQC theories/Wellfounded/Well_Ordering.v >COQC theories/Wellfounded/Wellfounded.v >COQC theories/Reals/Rdefinitions.v >COQC theories/Reals/Raxioms.v >COQC theories/Reals/Rpow_def.v >COQC contrib/setoid_ring/Field_theory.v >COQC contrib/setoid_ring/Field_tac.v >COQC contrib/setoid_ring/Field.v >COQC contrib/setoid_ring/RealField.v >COQC theories/Reals/RIneq.v >COQC theories/Reals/DiscrR.v >COQC theories/Reals/Rbase.v >COQC contrib/field/LegacyField_Compl.v >COQC contrib/ring/LegacyRing_theory.v >COQC contrib/ring/Quote.v >COQC contrib/ring/Ring_normalize.v >COQC contrib/ring/Ring_abstract.v >COQC contrib/ring/LegacyRing.v >COQC contrib/field/LegacyField_Theory.v >COQC contrib/field/LegacyField_Tactic.v >COQC contrib/field/LegacyField.v >COQC theories/Reals/LegacyRfield.v >COQC theories/Reals/R_Ifp.v >COQC contrib/fourier/Fourier_util.v >COQC contrib/fourier/Fourier.v >COQC theories/Reals/Rbasic_fun.v >COQC theories/Reals/R_sqr.v >COQC theories/Reals/SplitAbsolu.v >COQC theories/Reals/SplitRmult.v >COQC theories/Reals/ArithProp.v >COQC theories/Reals/Rfunctions.v >COQC theories/Reals/Rseries.v >COQC theories/Reals/SeqProp.v >COQC theories/Reals/Rcomplete.v >COQC theories/Reals/PartSum.v >COQC theories/Reals/AltSeries.v >COQC theories/Reals/Binomial.v >COQC theories/Reals/Rsigma.v >COQC theories/Reals/Rprod.v >COQC theories/Reals/Cauchy_prod.v >COQC theories/Reals/Alembert.v >COQC theories/Reals/SeqSeries.v >COQC theories/Reals/Rtrigo_fun.v >COQC theories/Reals/Rtrigo_def.v >COQC theories/Reals/Rtrigo_alt.v >COQC theories/Reals/Cos_rel.v >COQC theories/Reals/Cos_plus.v >COQC theories/Reals/Rtrigo.v >COQC theories/Reals/Rlimit.v >COQC theories/Reals/Rderiv.v >COQC theories/Reals/RList.v >COQC theories/Reals/Ranalysis1.v >Defining 'o' as keyword >COQC theories/Reals/Ranalysis2.v >COQC theories/Reals/Ranalysis3.v >COQC theories/Reals/Rtopology.v >COQC theories/Reals/MVT.v >COQC theories/Reals/PSeries_reg.v >COQC theories/Reals/Exp_prop.v >COQC theories/Reals/Rtrigo_reg.v >COQC theories/Reals/Rsqrt_def.v >COQC theories/Reals/R_sqrt.v >COQC theories/Reals/Rtrigo_calc.v >COQC theories/Reals/Rgeom.v >COQC theories/Reals/Sqrt_reg.v >COQC theories/Reals/Ranalysis4.v >COQC theories/Reals/Rpower.v >COQC theories/Reals/Ranalysis.v >COQC theories/Reals/NewtonInt.v >COQC theories/Reals/RiemannInt_SF.v >COQC theories/Reals/RiemannInt.v >COQC theories/Reals/Integration.v >COQC theories/Reals/Rlogic.v >COQC theories/Reals/Reals.v >COQC theories/Sorting/Heap.v >COQC theories/Sorting/PermutSetoid.v >COQC theories/Sorting/PermutEq.v >COQC theories/QArith/QArith_base.v >COQC theories/QArith/Qreduction.v >COQC theories/QArith/Qfield.v >COQC theories/QArith/Qring.v >COQC theories/QArith/Qreals.v >COQC theories/QArith/QArith.v >COQC theories/QArith/Qcanon.v >COQC theories/QArith/Qpower.v >COQC theories/QArith/Qabs.v >COQC theories/QArith/Qround.v >COQC theories/Numbers/NaryFunctions.v >COQC theories/Numbers/NumPrelude.v >COQC theories/Numbers/BigNumPrelude.v >COQC theories/Numbers/NatInt/NZAxioms.v >COQC theories/Numbers/Natural/Abstract/NAxioms.v >COQC theories/Numbers/NatInt/NZBase.v >COQC theories/Numbers/NatInt/NZAdd.v >COQC theories/Numbers/NatInt/NZMul.v >COQC theories/Numbers/NatInt/NZOrder.v >COQC theories/Numbers/NatInt/NZAddOrder.v >COQC theories/Numbers/NatInt/NZMulOrder.v >COQC theories/Numbers/Natural/Abstract/NBase.v >COQC theories/Numbers/Natural/Abstract/NAdd.v >COQC theories/Numbers/Natural/Abstract/NMul.v >COQC theories/Numbers/Natural/Abstract/NOrder.v >COQC theories/Numbers/Natural/Abstract/NAddOrder.v >COQC theories/Numbers/Natural/Abstract/NMulOrder.v >COQC theories/Numbers/Natural/Abstract/NSub.v >COQC theories/Numbers/Natural/Abstract/NIso.v >COQC theories/Numbers/Natural/Peano/NPeano.v >COQC theories/Numbers/Natural/Binary/NBinDefs.v >COQC theories/Numbers/Natural/Binary/NBinary.v >COQC theories/Numbers/Natural/SpecViaZ/NSig.v >COQC theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v >COQC theories/Numbers/Cyclic/DoubleCyclic/DoubleType.v >COQC theories/Numbers/Cyclic/DoubleCyclic/DoubleBase.v >COQC theories/Numbers/Cyclic/Abstract/CyclicAxioms.v >COQC theories/Numbers/Cyclic/DoubleCyclic/DoubleAdd.v >COQC theories/Numbers/Cyclic/DoubleCyclic/DoubleSub.v >COQC theories/Numbers/Cyclic/DoubleCyclic/DoubleMul.v >COQC theories/Numbers/Cyclic/DoubleCyclic/DoubleSqrt.v >COQC theories/Numbers/Cyclic/DoubleCyclic/DoubleLift.v >COQC theories/Numbers/Cyclic/DoubleCyclic/DoubleDivn1.v >COQC theories/Numbers/Cyclic/DoubleCyclic/DoubleDiv.v >COQC theories/Numbers/Cyclic/DoubleCyclic/DoubleCyclic.v >COQC theories/Numbers/Natural/BigN/Nbasic.v >COQC theories/Numbers/Natural/BigN/NMake.v >COQC theories/Numbers/Cyclic/Int31/Int31.v >COQC theories/Numbers/Cyclic/Int31/Cyclic31.v >COQC theories/Numbers/Natural/BigN/BigN.v >COQC theories/Numbers/Integer/Abstract/ZAxioms.v >COQC theories/Numbers/Integer/Abstract/ZBase.v >COQC theories/Numbers/Integer/Abstract/ZAdd.v >COQC theories/Numbers/Integer/Abstract/ZMul.v >COQC theories/Numbers/Integer/Abstract/ZLt.v >COQC theories/Numbers/Integer/Abstract/ZAddOrder.v >COQC theories/Numbers/Integer/Abstract/ZMulOrder.v >COQC theories/Numbers/Integer/Binary/ZBinary.v >COQC theories/Numbers/Integer/NatPairs/ZNatPairs.v >COQC theories/Numbers/Integer/SpecViaZ/ZSig.v >COQC theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v >COQC theories/Numbers/Integer/BigZ/ZMake.v >COQC theories/Numbers/Integer/BigZ/BigZ.v >COQC theories/Numbers/Cyclic/Abstract/NZCyclic.v >COQC theories/Numbers/Cyclic/ZModulo/ZModulo.v >COQC theories/Numbers/Rational/SpecViaQ/QSig.v >COQC theories/Numbers/Rational/BigQ/QMake.v >COQC theories/Numbers/Rational/BigQ/BigQ.v >COQC theories/Unicode/Utf8.v >COQC theories/Program/Utils.v >COQC theories/Program/Wf.v >COQC theories/Program/Equality.v >Defining 'refl' as keyword >COQC theories/Program/Subset.v >COQC theories/Program/Combinators.v >COQC theories/Program/Syntax.v >COQC theories/Program/Program.v >COQC theories/Classes/Morphisms_Relations.v >COQC theories/Classes/Functions.v >COQC theories/Classes/SetoidClass.v >COQC theories/Classes/SetoidAxioms.v >COQC theories/Classes/EquivDec.v >COQC theories/Classes/SetoidDec.v >COQC contrib/micromega/Refl.v >COQC contrib/micromega/CheckerMaker.v >COQC contrib/micromega/Env.v >COQC contrib/micromega/EnvRing.v >COQC contrib/micromega/OrderedRing.v >COQC contrib/micromega/Tauto.v >COQC contrib/micromega/RingMicromega.v >COQC contrib/micromega/VarMap.v >COQC contrib/micromega/ZCoeff.v >COQC contrib/micromega/ZMicromega.v >COQC contrib/micromega/QMicromega.v >COQC contrib/micromega/RMicromega.v >COQC contrib/micromega/Psatz.v >COQC contrib/ring/LegacyArithRing.v >COQC contrib/ring/LegacyNArithRing.v >COQC contrib/ring/LegacyZArithRing.v >COQC contrib/ring/Setoid_ring_theory.v >COQC contrib/ring/Setoid_ring_normalize.v >COQC contrib/ring/Setoid_ring.v >COQC contrib/rtauto/Bintree.v >COQC contrib/rtauto/Rtauto.v >COQC contrib/setoid_ring/Ring_equiv.v >COQC contrib/dp/Dp.v >OCAMLOPT4 tools/coq_makefile.ml4 >OCAMLOPT -o bin/coq_makefile >true bin/coq_makefile >OCAMLOPT tools/gallina_lexer.ml >OCAMLOPT tools/gallina.ml >OCAMLOPT -o bin/gallina >true bin/gallina >OCAMLOPT4 tools/coq-tex.ml4 >OCAMLOPT -o bin/coq-tex >true bin/coq-tex >OCAMLOPT tools/coqwc.ml >OCAMLOPT -o bin/coqwc >true bin/coqwc >OCAMLOPT tools/coqdoc/cdglobals.ml >OCAMLC tools/coqdoc/alpha.mli >OCAMLOPT tools/coqdoc/alpha.ml >OCAMLC tools/coqdoc/cdglobals.ml >OCAMLC tools/coqdoc/index.mli >OCAMLOPT tools/coqdoc/index.ml >OCAMLC tools/coqdoc/output.mli >OCAMLOPT tools/coqdoc/output.ml >OCAMLC tools/coqdoc/pretty.mli >OCAMLOPT tools/coqdoc/pretty.ml >OCAMLOPT tools/coqdoc/main.ml >OCAMLOPT -o bin/coqdoc >true bin/coqdoc >OCAMLC dev/top_printers.ml >OCAMLC dev/vm_printers.ml >OCAMLC lib/system.ml >OCAMLC lib/envars.ml >OCAMLC lib/bstack.ml >OCAMLC lib/edit.ml >OCAMLC lib/gset.ml >OCAMLC lib/gmap.ml >OCAMLC lib/tlm.ml >OCAMLC lib/gmapl.ml >OCAMLC lib/profile.ml >OCAMLC lib/explore.ml >OCAMLC lib/heap.ml >OCAMLC -a -o lib/lib.cma >OCAMLC library/decls.ml >OCAMLC library/heads.ml >OCAMLC pretyping/retyping.ml >OCAMLC pretyping/cbv.ml >OCAMLC pretyping/pretype_errors.ml >OCAMLC pretyping/recordops.ml >OCAMLC pretyping/typing.ml >OCAMLC pretyping/evarutil.ml >OCAMLC pretyping/evarconv.ml >OCAMLC pretyping/tacred.ml >OCAMLC pretyping/classops.ml >OCAMLC pretyping/typeclasses_errors.ml >OCAMLC pretyping/typeclasses.ml >OCAMLC pretyping/indrec.ml >OCAMLC pretyping/coercion.ml >OCAMLC pretyping/unification.ml >OCAMLC pretyping/cases.ml >OCAMLC pretyping/pretyping.ml >OCAMLC pretyping/clenv.ml >OCAMLC interp/notation.ml >OCAMLC interp/dumpglob.ml >OCAMLC interp/reserve.ml >OCAMLC library/impargs.ml >OCAMLC interp/constrextern.ml >OCAMLC interp/syntax_def.ml >OCAMLC interp/implicit_quantifiers.ml >OCAMLC interp/constrintern.ml >OCAMLC proofs/proof_trees.ml >OCAMLC proofs/proof_type.ml >OCAMLC proofs/logic.ml >OCAMLC proofs/refiner.ml >OCAMLC proofs/evar_refiner.ml >OCAMLC proofs/pfedit.ml >OCAMLC proofs/tactic_debug.ml >OCAMLC proofs/decl_mode.ml >OCAMLC parsing/ppconstr.ml >OCAMLC parsing/printer.ml >OCAMLC -rectypes parsing/pptactic.ml >OCAMLC parsing/ppdecl_proof.ml >OCAMLC parsing/tactic_printer.ml >OCAMLC parsing/egrammar.ml >OCAMLC toplevel/himsg.ml >OCAMLC toplevel/cerrors.ml >OCAMLC toplevel/vernacinterp.ml >Testing dev/printers.cma >OCAMLC -a dev/printers.cma >OCAMLOPT scripts/coqc.ml >OCAMLOPT -o bin/coqc.opt >true bin/coqc.opt >cd bin; ln -sf coqc.opt coqc >OCAMLC kernel/vm.ml >OCAMLC kernel/csymtable.ml >OCAMLC kernel/vconv.ml >OCAMLC -a -o kernel/kernel.cma >OCAMLC library/declaremods.ml >OCAMLC library/library.ml >OCAMLC library/states.ml >OCAMLC library/dischargedhypsmap.ml >OCAMLC -a -o library/library.cma >OCAMLC pretyping/vnorm.ml >OCAMLC pretyping/matching.ml >OCAMLC -a -o pretyping/pretyping.cma >OCAMLC interp/modintern.ml >OCAMLC interp/coqlib.ml >OCAMLC toplevel/discharge.ml >OCAMLC library/declare.ml >OCAMLC -a -o interp/interp.cma >OCAMLC proofs/redexpr.ml >OCAMLC proofs/tacmach.ml >OCAMLC proofs/clenvtac.ml >OCAMLC -a -o proofs/proofs.cma >OCAMLC4 parsing/g_xml.ml4 >OCAMLC parsing/printmod.ml >OCAMLC parsing/prettyp.ml >OCAMLC parsing/search.ml >OCAMLC -a -o parsing/parsing.cma >OCAMLC tactics/dn.ml >OCAMLC tactics/termdn.ml >OCAMLC tactics/btermdn.ml >OCAMLC tactics/nbtermdn.ml >OCAMLC tactics/tacticals.ml >OCAMLC4 tactics/hipattern.ml4 >OCAMLC tactics/tactics.ml >OCAMLC tactics/hiddentac.ml >OCAMLC tactics/elim.ml >OCAMLC tactics/dhyp.ml >OCAMLC tactics/auto.ml >OCAMLC toplevel/ind_tables.ml >OCAMLC tactics/equality.ml >OCAMLC tactics/contradiction.ml >OCAMLC tactics/inv.ml >OCAMLC tactics/leminv.ml >OCAMLC tactics/tacinterp.ml >OCAMLC tactics/autorewrite.ml >OCAMLC tactics/evar_tactics.ml >OCAMLC tactics/decl_interp.ml >OCAMLC tactics/decl_proof_instr.ml >OCAMLC -a -o tactics/tactics.cma >OCAMLC toplevel/class.ml >OCAMLC toplevel/metasyntax.ml >OCAMLC toplevel/auto_ind_decl.ml >OCAMLC toplevel/command.ml >OCAMLC toplevel/record.ml >OCAMLC parsing/ppvernac.ml >OCAMLC toplevel/classes.ml >CAMLP4O toplevel/mltop.ml4 >OCAMLC toplevel/mltop.byteml >OCAMLC toplevel/vernacentries.ml >OCAMLC4 toplevel/whelp.ml4 >OCAMLC toplevel/vernac.ml >OCAMLC toplevel/line_oriented_parser.ml >OCAMLC toplevel/protectedtoplevel.ml >OCAMLC toplevel/toplevel.ml >OCAMLC toplevel/usage.ml >OCAMLC toplevel/coqinit.ml >OCAMLC toplevel/coqtop.ml >OCAMLC -a -o toplevel/toplevel.cma >OCAMLC4 parsing/g_vernac.ml4 >OCAMLC4 parsing/g_proofs.ml4 >OCAMLC parsing/g_natsyntax.ml >OCAMLC parsing/g_zsyntax.ml >OCAMLC parsing/g_rsyntax.ml >OCAMLC parsing/g_ascii_syntax.ml >OCAMLC parsing/g_string_syntax.ml >OCAMLC4 parsing/g_decl_mode.ml4 >OCAMLC parsing/g_intsyntax.ml >OCAMLC -a -o parsing/highparsing.cma >OCAMLC tactics/refine.ml >OCAMLC4 tactics/extraargs.ml4 >OCAMLC4 tactics/extratactics.ml4 >OCAMLC4 tactics/eauto.ml4 >OCAMLC4 tactics/class_tactics.ml4 >OCAMLC4 tactics/tauto.ml4 >OCAMLC4 tactics/eqdecide.ml4 >OCAMLC -a -o tactics/hightactics.cma >OCAMLC contrib/omega/omega.ml >OCAMLC contrib/omega/coq_omega.ml >OCAMLC4 contrib/omega/g_omega.ml4 >OCAMLC contrib/romega/const_omega.ml >OCAMLC contrib/romega/refl_omega.ml >OCAMLC4 contrib/romega/g_romega.ml4 >OCAMLC contrib/micromega/mutils.ml >OCAMLC contrib/micromega/vector.ml >OCAMLC contrib/micromega/micromega.ml >OCAMLC contrib/micromega/mfourier.ml >OCAMLC contrib/micromega/certificate.ml >OCAMLC contrib/micromega/coq_micromega.ml >OCAMLC contrib/ring/quote.ml >OCAMLC contrib/ring/ring.ml >OCAMLC4 contrib/micromega/g_micromega.ml4 >OCAMLC4 contrib/ring/g_quote.ml4 >OCAMLC4 contrib/ring/g_ring.ml4 >OCAMLC4 contrib/setoid_ring/newring.ml4 >OCAMLC contrib/dp/dp_why.ml >OCAMLC contrib/dp/dp_zenon.ml >OCAMLC contrib/dp/dp.ml >OCAMLC contrib/dp/dp_gappa.ml >OCAMLC4 contrib/dp/g_dp.ml4 >OCAMLC4 contrib/field/field.ml4 >OCAMLC contrib/fourier/fourier.ml >OCAMLC contrib/fourier/fourierR.ml >OCAMLC4 contrib/fourier/g_fourier.ml4 >OCAMLC contrib/extraction/table.ml >OCAMLC contrib/extraction/mlutil.ml >OCAMLC contrib/extraction/modutil.ml >OCAMLC contrib/extraction/extraction.ml >OCAMLC contrib/extraction/common.ml >OCAMLC contrib/extraction/ocaml.ml >OCAMLC contrib/extraction/haskell.ml >OCAMLC contrib/extraction/scheme.ml >OCAMLC contrib/extraction/extract_env.ml >OCAMLC4 contrib/extraction/g_extraction.ml4 >OCAMLC contrib/xml/unshare.ml >OCAMLC4 contrib/xml/xml.ml4 >OCAMLC contrib/xml/doubleTypeInference.ml >OCAMLC contrib/xml/cic2acic.ml >OCAMLC4 contrib/xml/acic2Xml.ml4 >OCAMLC contrib/xml/xmlcommand.ml >OCAMLC4 contrib/xml/proofTree2Xml.ml4 >OCAMLC4 contrib/xml/xmlentries.ml4 >OCAMLC contrib/xml/cic2Xml.ml >OCAMLC4 contrib/xml/dumptree.ml4 >OCAMLC contrib/cc/ccalgo.ml >OCAMLC contrib/cc/ccproof.ml >OCAMLC contrib/cc/cctac.ml >OCAMLC4 contrib/cc/g_congruence.ml4 >OCAMLC contrib/firstorder/formula.ml >OCAMLC contrib/firstorder/unify.ml >OCAMLC contrib/firstorder/sequent.ml >OCAMLC contrib/firstorder/rules.ml >OCAMLC contrib/firstorder/instances.ml >OCAMLC contrib/firstorder/ground.ml >OCAMLC4 contrib/firstorder/g_ground.ml4 >OCAMLC contrib/subtac/subtac_utils.ml >OCAMLC contrib/subtac/eterm.ml >OCAMLC4 contrib/subtac/g_eterm.ml4 >OCAMLC contrib/subtac/subtac_errors.ml >OCAMLC contrib/subtac/subtac_coercion.ml >OCAMLC contrib/subtac/subtac_obligations.ml >OCAMLC contrib/subtac/subtac_cases.ml >OCAMLC contrib/subtac/subtac_pretyping_F.ml >OCAMLC contrib/subtac/subtac_pretyping.ml >OCAMLC contrib/subtac/subtac_command.ml >OCAMLC contrib/subtac/subtac_classes.ml >OCAMLC contrib/subtac/subtac.ml >OCAMLC4 contrib/subtac/g_subtac.ml4 >OCAMLC4 contrib/subtac/equations.ml4 >OCAMLC contrib/rtauto/proof_search.ml >OCAMLC contrib/rtauto/refl_tauto.ml >OCAMLC4 contrib/rtauto/g_rtauto.ml4 >OCAMLC contrib/funind/indfun_common.ml >OCAMLC contrib/funind/rawtermops.ml >OCAMLC contrib/funind/recdef.ml >OCAMLC contrib/funind/rawterm_to_relation.ml >OCAMLC contrib/funind/functional_principles_proofs.ml >OCAMLC contrib/funind/functional_principles_types.ml >OCAMLC contrib/funind/invfun.ml >OCAMLC contrib/funind/indfun.ml >OCAMLC contrib/funind/merge.ml >OCAMLC4 contrib/funind/g_indfun.ml4 >OCAMLC -a -o contrib/contrib.cma >COQMKTOP -o bin/coqtop.byte >cd bin; ln -sf coqtop.opt coqtop >OCAMLC checker/validate.ml >OCAMLC checker/term.mli >OCAMLC checker/term.ml >OCAMLC checker/declarations.mli >OCAMLC checker/declarations.ml >OCAMLC checker/environ.mli >OCAMLC checker/environ.ml >OCAMLC checker/closure.mli >OCAMLC checker/closure.ml >OCAMLC checker/reduction.mli >OCAMLC checker/reduction.ml >OCAMLC checker/type_errors.mli >OCAMLC checker/type_errors.ml >OCAMLC checker/modops.mli >OCAMLC checker/modops.ml >OCAMLC checker/inductive.mli >OCAMLC checker/inductive.ml >OCAMLC checker/typeops.mli >OCAMLC checker/typeops.ml >OCAMLC checker/indtypes.mli >OCAMLC checker/indtypes.ml >OCAMLC checker/subtyping.mli >OCAMLC checker/subtyping.ml >OCAMLC checker/mod_checking.ml >OCAMLC checker/safe_typing.mli >OCAMLC checker/safe_typing.ml >OCAMLC checker/check.ml >OCAMLC checker/check_stat.mli >OCAMLC checker/check_stat.ml >OCAMLC checker/checker.ml >OCAMLC -a -o checker/check.cma >OCAMLC -o bin/coqchk.byte >OCAMLOPT checker/validate.ml >OCAMLOPT checker/term.ml >OCAMLOPT checker/declarations.ml >OCAMLOPT checker/environ.ml >OCAMLOPT checker/closure.ml >OCAMLOPT checker/reduction.ml >OCAMLOPT checker/type_errors.ml >OCAMLOPT checker/modops.ml >OCAMLOPT checker/inductive.ml >OCAMLOPT checker/typeops.ml >OCAMLOPT checker/indtypes.ml >OCAMLOPT checker/subtyping.ml >OCAMLOPT checker/mod_checking.ml >OCAMLOPT checker/safe_typing.ml >OCAMLOPT checker/check.ml >OCAMLOPT checker/check_stat.ml >OCAMLOPT checker/checker.ml >OCAMLOPT -a -o checker/check.cmxa >OCAMLOPT -o bin/coqchk.opt >true bin/coqchk.opt >cd bin && ln -sf coqchk.opt coqchk >OCAMLOPT contrib/micromega/csdpcert.ml >OCAMLOPT -o contrib/micromega/csdpcert >true contrib/micromega/csdpcert >OCAMLC ide/utils/okey.mli >OCAMLC ide/utils/okey.ml >OCAMLC ide/utils/config_file.mli >OCAMLC ide/utils/config_file.ml >OCAMLC ide/utils/configwin_keys.ml >OCAMLC ide/utils/configwin_types.ml >OCAMLC ide/utils/configwin_messages.ml >OCAMLC ide/utils/configwin_ihm.ml >OCAMLC ide/utils/configwin.mli >OCAMLC ide/utils/configwin.ml >OCAMLC ide/utils/editable_cells.ml >OCAMLC ide/config_parser.mli >OCAMLC ide/config_parser.ml >OCAMLC ide/config_lexer.ml >OCAMLC ide/utf8_convert.ml >OCAMLC ide/preferences.mli >OCAMLC ide/preferences.ml >OCAMLC ide/ideutils.mli >OCAMLC ide/ideutils.ml >OCAMLC ide/coq.mli >OCAMLC ide/blaster_window.ml >OCAMLC ide/undo.mli >OCAMLC ide/undo.ml >OCAMLC ide/find_phrase.ml >OCAMLC ide/highlight.ml >OCAMLC ide/coq.ml >OCAMLC ide/coq_commands.ml >OCAMLC ide/coq_tactics.mli >OCAMLC ide/coq_tactics.ml >OCAMLC ide/command_windows.mli >OCAMLC ide/command_windows.ml >OCAMLC ide/coqide.mli >OCAMLC ide/coqide.ml >OCAMLC -a -o ide/ide.cma >COQMKTOP -o bin/coqide.byte >OCAMLOPT ide/utils/okey.ml >OCAMLOPT ide/utils/config_file.ml >OCAMLOPT ide/utils/configwin_keys.ml >OCAMLOPT ide/utils/configwin_types.ml >OCAMLOPT ide/utils/configwin_messages.ml >OCAMLOPT ide/utils/configwin_ihm.ml >OCAMLOPT ide/utils/configwin.ml >OCAMLOPT ide/utils/editable_cells.ml >OCAMLOPT ide/config_parser.ml >OCAMLOPT ide/config_lexer.ml >OCAMLOPT ide/utf8_convert.ml >OCAMLOPT ide/preferences.ml >OCAMLOPT ide/ideutils.ml >OCAMLOPT ide/coq.ml >OCAMLOPT ide/blaster_window.ml >OCAMLOPT ide/undo.ml >OCAMLOPT ide/find_phrase.ml >OCAMLOPT ide/highlight.ml >OCAMLOPT ide/coq_commands.ml >OCAMLOPT ide/coq_tactics.ml >OCAMLOPT ide/command_windows.ml >OCAMLOPT ide/coqide.ml >OCAMLOPT -a -o ide/ide.cmxa >COQMKTOP -o bin/coqide.opt >true bin/coqide.opt >cd bin; ln -sf coqide.opt coqide >OCAMLC contrib/interface/ascent.mli >OCAMLC contrib/interface/vtp.mli >OCAMLC contrib/interface/vtp.ml >OCAMLC contrib/interface/xlate.mli >OCAMLC contrib/interface/xlate.ml >OCAMLC contrib/interface/paths.mli >OCAMLC contrib/interface/paths.ml >OCAMLC contrib/interface/translate.mli >OCAMLC contrib/interface/translate.ml >OCAMLC contrib/interface/pbp.mli >OCAMLC contrib/interface/pbp.ml >OCAMLC contrib/interface/dad.mli >OCAMLC contrib/interface/dad.ml >OCAMLC contrib/interface/history.mli >OCAMLC contrib/interface/history.ml >OCAMLC contrib/interface/name_to_ast.mli >OCAMLC contrib/interface/name_to_ast.ml >OCAMLC contrib/interface/debug_tac.mli >OCAMLC4 contrib/interface/debug_tac.ml4 >OCAMLC contrib/interface/showproof_ct.ml >OCAMLC contrib/interface/showproof.mli >OCAMLC contrib/interface/showproof.ml >OCAMLC contrib/interface/blast.mli >OCAMLC contrib/interface/blast.ml >OCAMLC contrib/interface/depends.ml >OCAMLC4 contrib/interface/centaur.ml4 >COQMKTOP -o bin/coq-interface >OCAMLOPT contrib/interface/vtp.ml >OCAMLOPT contrib/interface/xlate.ml >OCAMLOPT contrib/interface/paths.ml >OCAMLOPT contrib/interface/translate.ml >OCAMLOPT contrib/interface/pbp.ml >OCAMLOPT contrib/interface/dad.ml >OCAMLOPT contrib/interface/history.ml >OCAMLOPT contrib/interface/name_to_ast.ml >OCAMLOPT4 contrib/interface/debug_tac.ml4 >OCAMLOPT contrib/interface/showproof_ct.ml >OCAMLOPT contrib/interface/showproof.ml >OCAMLOPT contrib/interface/blast.ml >OCAMLOPT contrib/interface/depends.ml >OCAMLOPT4 contrib/interface/centaur.ml4 >COQMKTOP -o bin/coq-interface.opt >OCAMLC contrib/interface/line_parser.mli >OCAMLC4 contrib/interface/line_parser.ml4 >OCAMLC contrib/interface/parse.ml >OCAMLC -o bin/coq-parser >OCAMLOPT4 contrib/interface/line_parser.ml4 >OCAMLOPT contrib/interface/parse.ml >OCAMLOPT -o bin/coq-parser.opt >install -m 644 doc/common/styles/html/simple/styles.hva doc/refman >printf '\\newcommand{\\coqversion}{8.2pl1}' > doc/common/version.tex >(cd `dirname doc/refman/RefMan-gal.tex`; /var/tmp/portage/sci-mathematics/coq-8.2_p1-r1/work/coq-8.2pl1/bin/coq-tex -n 72 -image "/var/tmp/portage/sci-mathematics/coq-8.2_p1-r1/work/coq-8.2pl1/bin/coqtop -boot" -sl -small `basename doc/refman/RefMan-gal.tex`) >Your version of coqtop seems OK >(cd `dirname doc/refman/RefMan-ext.tex`; /var/tmp/portage/sci-mathematics/coq-8.2_p1-r1/work/coq-8.2pl1/bin/coq-tex -n 72 -image "/var/tmp/portage/sci-mathematics/coq-8.2_p1-r1/work/coq-8.2pl1/bin/coqtop -boot" -sl -small `basename doc/refman/RefMan-ext.tex`) >Your version of coqtop seems OK >(cd `dirname doc/refman/RefMan-mod.tex`; /var/tmp/portage/sci-mathematics/coq-8.2_p1-r1/work/coq-8.2pl1/bin/coq-tex -n 72 -image "/var/tmp/portage/sci-mathematics/coq-8.2_p1-r1/work/coq-8.2pl1/bin/coqtop -boot" -sl -small `basename doc/refman/RefMan-mod.tex`) >Your version of coqtop seems OK >(cd `dirname doc/refman/RefMan-tac.tex`; /var/tmp/portage/sci-mathematics/coq-8.2_p1-r1/work/coq-8.2pl1/bin/coq-tex -n 72 -image "/var/tmp/portage/sci-mathematics/coq-8.2_p1-r1/work/coq-8.2pl1/bin/coqtop -boot" -sl -small `basename doc/refman/RefMan-tac.tex`) >Your version of coqtop seems OK >(cd `dirname doc/refman/RefMan-cic.tex`; /var/tmp/portage/sci-mathematics/coq-8.2_p1-r1/work/coq-8.2pl1/bin/coq-tex -n 72 -image "/var/tmp/portage/sci-mathematics/coq-8.2_p1-r1/work/coq-8.2pl1/bin/coqtop -boot" -sl -small `basename doc/refman/RefMan-cic.tex`) >Your version of coqtop seems OK >(cd `dirname doc/refman/RefMan-lib.tex`; /var/tmp/portage/sci-mathematics/coq-8.2_p1-r1/work/coq-8.2pl1/bin/coq-tex -n 72 -image "/var/tmp/portage/sci-mathematics/coq-8.2_p1-r1/work/coq-8.2pl1/bin/coqtop -boot" -sl -small `basename doc/refman/RefMan-lib.tex`) >Your version of coqtop seems OK >(cd `dirname doc/refman/RefMan-tacex.tex`; /var/tmp/portage/sci-mathematics/coq-8.2_p1-r1/work/coq-8.2pl1/bin/coq-tex -n 72 -image "/var/tmp/portage/sci-mathematics/coq-8.2_p1-r1/work/coq-8.2pl1/bin/coqtop -boot" -sl -small `basename doc/refman/RefMan-tacex.tex`) >Your version of coqtop seems OK >(cd `dirname doc/refman/RefMan-syn.tex`; /var/tmp/portage/sci-mathematics/coq-8.2_p1-r1/work/coq-8.2pl1/bin/coq-tex -n 72 -image "/var/tmp/portage/sci-mathematics/coq-8.2_p1-r1/work/coq-8.2pl1/bin/coqtop -boot" -sl -small `basename doc/refman/RefMan-syn.tex`) >Your version of coqtop seems OK >(cd `dirname doc/refman/RefMan-oth.tex`; /var/tmp/portage/sci-mathematics/coq-8.2_p1-r1/work/coq-8.2pl1/bin/coq-tex -n 72 -image "/var/tmp/portage/sci-mathematics/coq-8.2_p1-r1/work/coq-8.2pl1/bin/coqtop -boot" -sl -small `basename doc/refman/RefMan-oth.tex`) >Your version of coqtop seems OK >(cd `dirname doc/refman/RefMan-ltac.tex`; /var/tmp/portage/sci-mathematics/coq-8.2_p1-r1/work/coq-8.2pl1/bin/coq-tex -n 72 -image "/var/tmp/portage/sci-mathematics/coq-8.2_p1-r1/work/coq-8.2pl1/bin/coqtop -boot" -sl -small `basename doc/refman/RefMan-ltac.tex`) >Your version of coqtop seems OK >(cd `dirname doc/refman/RefMan-decl.tex`; /var/tmp/portage/sci-mathematics/coq-8.2_p1-r1/work/coq-8.2pl1/bin/coq-tex -n 72 -image "/var/tmp/portage/sci-mathematics/coq-8.2_p1-r1/work/coq-8.2pl1/bin/coqtop -boot" -sl -small `basename doc/refman/RefMan-decl.tex`) >Your version of coqtop seems OK >(cd `dirname doc/refman/Cases.tex`; /var/tmp/portage/sci-mathematics/coq-8.2_p1-r1/work/coq-8.2pl1/bin/coq-tex -n 72 -image "/var/tmp/portage/sci-mathematics/coq-8.2_p1-r1/work/coq-8.2pl1/bin/coqtop -boot" -sl -small `basename doc/refman/Cases.tex`) >Your version of coqtop seems OK >(cd `dirname doc/refman/Coercion.tex`; /var/tmp/portage/sci-mathematics/coq-8.2_p1-r1/work/coq-8.2pl1/bin/coq-tex -n 72 -image "/var/tmp/portage/sci-mathematics/coq-8.2_p1-r1/work/coq-8.2pl1/bin/coqtop -boot" -sl -small `basename doc/refman/Coercion.tex`) >Your version of coqtop seems OK >(cd `dirname doc/refman/Extraction.tex`; /var/tmp/portage/sci-mathematics/coq-8.2_p1-r1/work/coq-8.2pl1/bin/coq-tex -n 72 -image "/var/tmp/portage/sci-mathematics/coq-8.2_p1-r1/work/coq-8.2pl1/bin/coqtop -boot" -sl -small `basename doc/refman/Extraction.tex`) >Your version of coqtop seems OK >(cd `dirname doc/refman/Program.tex`; /var/tmp/portage/sci-mathematics/coq-8.2_p1-r1/work/coq-8.2pl1/bin/coq-tex -n 72 -image "/var/tmp/portage/sci-mathematics/coq-8.2_p1-r1/work/coq-8.2pl1/bin/coqtop -boot" -sl -small `basename doc/refman/Program.tex`) >Your version of coqtop seems OK >(cd `dirname doc/refman/Omega.tex`; /var/tmp/portage/sci-mathematics/coq-8.2_p1-r1/work/coq-8.2pl1/bin/coq-tex -n 72 -image "/var/tmp/portage/sci-mathematics/coq-8.2_p1-r1/work/coq-8.2pl1/bin/coqtop -boot" -sl -small `basename doc/refman/Omega.tex`) >Your version of coqtop seems OK >(cd `dirname doc/refman/Micromega.tex`; /var/tmp/portage/sci-mathematics/coq-8.2_p1-r1/work/coq-8.2pl1/bin/coq-tex -n 72 -image "/var/tmp/portage/sci-mathematics/coq-8.2_p1-r1/work/coq-8.2pl1/bin/coqtop -boot" -sl -small `basename doc/refman/Micromega.tex`) >Your version of coqtop seems OK >(cd `dirname doc/refman/Polynom.tex`; /var/tmp/portage/sci-mathematics/coq-8.2_p1-r1/work/coq-8.2pl1/bin/coq-tex -n 72 -image "/var/tmp/portage/sci-mathematics/coq-8.2_p1-r1/work/coq-8.2pl1/bin/coqtop -boot" -sl -small `basename doc/refman/Polynom.tex`) >Your version of coqtop seems OK >(cd `dirname doc/refman/Setoid.tex`; /var/tmp/portage/sci-mathematics/coq-8.2_p1-r1/work/coq-8.2pl1/bin/coq-tex -n 72 -image "/var/tmp/portage/sci-mathematics/coq-8.2_p1-r1/work/coq-8.2pl1/bin/coqtop -boot" -sl -small `basename doc/refman/Setoid.tex`) >Your version of coqtop seems OK >(cd `dirname doc/refman/Classes.tex`; /var/tmp/portage/sci-mathematics/coq-8.2_p1-r1/work/coq-8.2pl1/bin/coq-tex -n 72 -image "/var/tmp/portage/sci-mathematics/coq-8.2_p1-r1/work/coq-8.2pl1/bin/coqtop -boot" -sl -small `basename doc/refman/Classes.tex`) >Your version of coqtop seems OK >pngtopnm doc/refman/coqide.png | pnmtops -equalpixels -noturn -rle > doc/refman/coqide.eps >pnmtops: generating color Postscript program. >pngtopnm doc/refman/coqide-queries.png | pnmtops -equalpixels -noturn -rle > doc/refman/coqide-queries.eps >pnmtops: generating color Postscript program. >This is pdfTeXk, Version 3.1415926-1.40.9 (Web2C 7.5.7) > %&-line parsing enabled. >entering extended mode >LaTeX Warning: Label(s) may have changed. Rerun to get cross-references right. >(cd doc/refman; BIBINPUTS=.: hevea -fix -exec xxdate.exe ./styles.hva ./Reference-Manual.tex) >Exclude comment 'comment' >./RefMan-int.tex:9: Warning: Undefined citation: 'CoqArt' >./RefMan-int.tex:50: Warning: Undefined label: 'Addoc-coqc' >./RefMan-int.tex:54: Warning: Undefined citation: 'ProofGeneral' >./RefMan-int.tex:55: Warning: Undefined citation: 'Pcoq' >./RefMan-int.tex:57: Warning: Undefined label: 'Addoc-coqide' >./RefMan-int.tex:67: Warning: Undefined label: 'Gallina' >./RefMan-int.tex:67: Warning: Undefined label: 'Gallina-extension' >./RefMan-int.tex:70: Warning: Undefined label: 'Theories' >./RefMan-int.tex:71: Warning: Undefined label: 'Cic' >./RefMan-int.tex:72: Warning: Undefined label: 'chapter:Modules' >./RefMan-int.tex:75: Warning: Undefined label: 'Vernacular-commands' >./RefMan-int.tex:80: Warning: Undefined label: 'Proof-handling' >./RefMan-int.tex:81: Warning: Undefined label: 'Tactics' >./RefMan-int.tex:84: Warning: Undefined label: 'TacticLanguage' >./RefMan-int.tex:85: Warning: Undefined label: 'Tactics-examples' >./RefMan-int.tex:93: Warning: Undefined label: 'Addoc-syntax' >./RefMan-int.tex:96: Warning: Undefined label: 'Addoc-coqc' >./RefMan-int.tex:98: Warning: Undefined label: 'Utilities' >./RefMan-int.tex:101: Warning: Undefined label: 'Addoc-coqide' >./RefMan-gal.v.tex:10: Warning: Undefined label: 'term' >./RefMan-gal.v.tex:12: Warning: Undefined label: 'Vernacular' >./RefMan-gal.v.tex:16: Warning: Undefined label: 'Cic' >./RefMan-gal.v.tex:220: Warning: Undefined label: 'term-syntax' >./RefMan-gal.v.tex:220: Warning: Undefined label: 'term-syntax-aux' >./RefMan-gal.v.tex:223: Warning: Undefined label: 'Cic' >./RefMan-gal.v.tex:224: Warning: Undefined label: 'Gallina-extension' >./RefMan-gal.v.tex:225: Warning: Undefined label: 'Addoc-syntax' >./RefMan-gal.v.tex:231: Warning: Undefined label: 'products' >./RefMan-gal.v.tex:232: Warning: Undefined label: 'abstractions' >./RefMan-gal.v.tex:233: Warning: Undefined label: 'fixpoints' >./RefMan-gal.v.tex:234: Warning: Undefined label: 'fixpoints' >./RefMan-gal.v.tex:236: Warning: Undefined label: 'let-in' >./RefMan-gal.v.tex:237: Warning: Undefined label: 'fixpoints' >./RefMan-gal.v.tex:239: Warning: Undefined label: 'fixpoints' >./RefMan-gal.v.tex:242: Warning: Undefined label: 'caseanalysis' >./RefMan-gal.v.tex:242: Warning: Undefined label: 'Mult-match' >./RefMan-gal.v.tex:244: Warning: Undefined label: 'caseanalysis' >./RefMan-gal.v.tex:244: Warning: Undefined label: 'Mult-match' >./RefMan-gal.v.tex:245: Warning: Undefined label: 'typecast' >./RefMan-gal.v.tex:246: Warning: Undefined label: 'products' >./RefMan-gal.v.tex:247: Warning: Undefined label: 'applications' >./RefMan-gal.v.tex:249: Warning: Undefined label: 'Implicits-explicitation' >./RefMan-gal.v.tex:250: Warning: Undefined label: 'scopechange' >./RefMan-gal.v.tex:254: Warning: Undefined label: 'caseanalysis' >./RefMan-gal.v.tex:255: Warning: Undefined label: 'qualid' >./RefMan-gal.v.tex:256: Warning: Undefined label: 'Gallina-sorts' >./RefMan-gal.v.tex:257: Warning: Undefined label: 'numerals' >./RefMan-gal.v.tex:258: Warning: Undefined label: 'hole' >./RefMan-gal.v.tex:262: Warning: Undefined label: 'Implicits-explicitation' >./RefMan-gal.v.tex:266: Warning: Undefined label: 'Binders' >./RefMan-gal.v.tex:269: Warning: Undefined label: 'Binders' >./RefMan-gal.v.tex:272: Warning: Undefined label: 'Binders' >./RefMan-gal.v.tex:367: Warning: Undefined label: 'Addoc-syntax' >./RefMan-gal.v.tex:369: Warning: Undefined label: 'libnats' >./RefMan-gal.v.tex:397: Warning: Undefined label: 'Sorts' >./RefMan-gal.v.tex:446: Warning: Undefined label: 'Binders' >./RefMan-gal.v.tex:453: Warning: Undefined label: 'let-in' >./RefMan-gal.v.tex:493: Warning: Undefined label: 'Implicits-explicitation' >./RefMan-gal.v.tex:535: Warning: Undefined label: 'Mult-match' >./RefMan-gal.v.tex:535: Warning: Undefined label: 'Mult-match-full' >./RefMan-gal.v.tex:607: Warning: Undefined label: 'Equality' >./RefMan-gal.v.tex:610: Warning: Undefined label: 'listn' >./RefMan-gal.v.tex:653: Warning: Undefined label: 'if-then-else' >./RefMan-gal.v.tex:653: Warning: Undefined label: 'Letin' >./RefMan-gal.v.tex:666: Warning: Undefined label: 'Fixpoint' >./RefMan-gal.v.tex:674: Warning: Undefined label: 'CoFixpoint' >./RefMan-gal.v.tex:740: Warning: Undefined label: 'sentences-syntax' >./RefMan-gal.v.tex:806: Warning: Undefined label: 'Section' >./RefMan-gal.v.tex:850: Warning: Undefined label: 'delta' >./RefMan-gal.v.tex:858: Warning: Undefined label: 'Typed-terms' >./RefMan-gal.v.tex:895: Warning: Undefined label: 'Opaque' >./RefMan-gal.v.tex:895: Warning: Undefined label: 'Transparent' >./RefMan-gal.v.tex:895: Warning: Undefined label: 'unfold' >./RefMan-gal.v.tex:915: Warning: Undefined label: 'Section' >./RefMan-gal.v.tex:915: Warning: Undefined label: 'Opaque' >./RefMan-gal.v.tex:916: Warning: Undefined label: 'Transparent' >./RefMan-gal.v.tex:916: Warning: Undefined label: 'unfold' >./RefMan-gal.v.tex:953: Warning: Undefined label: 'Positivity' >./RefMan-gal.v.tex:1182: Warning: Undefined label: 'Cic-inductive-definitions' >./RefMan-gal.v.tex:1182: Warning: Undefined label: 'Tac-induction' >./RefMan-gal.v.tex:1309: Warning: Undefined label: 'Section' >./RefMan-gal.v.tex:1335: Warning: Undefined label: 'gal_Inductive_Definitions' >./RefMan-gal.v.tex:1369: Warning: Undefined label: 'CoFixpoint' >./RefMan-gal.v.tex:1379: Warning: Undefined label: 'Function' >./RefMan-gal.v.tex:1432: Warning: Undefined label: 'Caseexpr' >./RefMan-gal.v.tex:1535: Warning: Undefined label: 'Scheme' >./RefMan-gal.v.tex:1547: Warning: Undefined label: 'CoInductiveTypes' >./RefMan-gal.v.tex:1612: Warning: Undefined label: 'Fixpoint' >./RefMan-gal.v.tex:1623: Warning: Undefined label: 'Proof-handling' >./RefMan-gal.v.tex:1659: Warning: Undefined label: 'Fixpoint' >./RefMan-gal.v.tex:1660: Warning: Undefined label: 'CoFixpoint' >./RefMan-gal.v.tex:1673: Warning: Undefined label: 'Guarded' >./RefMan-gal.v.tex:1682: Warning: Undefined label: 'Transparent' >./RefMan-gal.v.tex:1682: Warning: Undefined label: 'unfold' >./RefMan-gal.v.tex:1696: Warning: Undefined label: 'Tactics' >./RefMan-gal.v.tex:1697: Warning: Undefined label: 'Proof-handling' >./RefMan-gal.v.tex:1715: Warning: Undefined label: 'Opaque' >./RefMan-gal.v.tex:1716: Warning: Undefined label: 'Conversion-tactics' >./RefMan-gal.v.tex:1724: Warning: Undefined label: 'Transparent' >./RefMan-gal.v.tex:1725: Warning: Undefined label: 'Conversion-tactics' >./RefMan-ext.v.tex:12: Warning: Undefined label: 'record-syntax' >./RefMan-ext.v.tex:190: Warning: Undefined label: 'Axiom' >./RefMan-ext.v.tex:192: Warning: Undefined label: 'Fixpoint' >./RefMan-ext.v.tex:192: Warning: Undefined label: 'Caseexpr' >./RefMan-ext.v.tex:206: Warning: Undefined label: 'gal_Inductive_Definitions' >./RefMan-ext.v.tex:210: Warning: Undefined label: 'Coercions-and-records' >./RefMan-ext.v.tex:233: Warning: Undefined label: 'fig:projsyntax' >./RefMan-ext.v.tex:263: Warning: Undefined label: 'SetPrintingMatching' >./RefMan-ext.v.tex:265: Warning: Undefined label: 'Mult-match-full' >./RefMan-ext.v.tex:324: Warning: Undefined label: 'printing-options' >./RefMan-ext.v.tex:365: Warning: Undefined label: 'printing-options' >./RefMan-ext.v.tex:409: Warning: Undefined label: 'printing-options' >./RefMan-ext.v.tex:663: Warning: Undefined label: 'FunInduction' >./RefMan-ext.v.tex:678: Warning: Undefined label: 'FunInduction' >./RefMan-ext.v.tex:679: Warning: Undefined label: 'FunScheme' >./RefMan-ext.v.tex:679: Warning: Undefined label: 'FunScheme-examples' >./RefMan-ext.v.tex:747: Warning: Undefined label: 'FunScheme' >./RefMan-ext.v.tex:747: Warning: Undefined label: 'FunScheme-examples' >./RefMan-ext.v.tex:747: Warning: Undefined label: 'FunInduction' >./RefMan-ext.v.tex:763: Warning: Undefined label: 'Inductive' >./RefMan-ext.v.tex:853: Warning: Undefined label: 'Simpl-definitions' >./RefMan-mod.v.tex:446: Warning: Undefined label: 'Notation' >./RefMan-ext.v.tex:949: Warning: Undefined label: 'qualid' >./RefMan-ext.v.tex:956: Warning: Undefined label: 'coqoptions' >./RefMan-ext.v.tex:958: Warning: Undefined label: 'coqoptions' >./RefMan-ext.v.tex:966: Warning: Undefined label: 'AddLoadPath' >./RefMan-ext.v.tex:966: Warning: Undefined label: 'AddRecLoadPath' >./RefMan-ext.v.tex:1004: Warning: Undefined label: 'Require' >./RefMan-ext.v.tex:1005: Warning: Undefined label: 'Import' >./RefMan-ext.v.tex:1048: Warning: Undefined label: 'Locate' >./RefMan-ext.v.tex:1049: Warning: Undefined label: 'Locate Library' >./RefMan-ext.v.tex:1147: Warning: Undefined label: 'SetReversiblePatternImplicit' >./RefMan-ext.v.tex:1167: Warning: Undefined label: 'ImplicitArguments' >./RefMan-ext.v.tex:1169: Warning: Undefined label: 'SetMaximalImplicitInsertion' >./RefMan-ext.v.tex:1170: Warning: Undefined label: 'PrintImplicit' >./RefMan-ext.v.tex:1328: Warning: Undefined label: 'PrintImplicit' >./RefMan-ext.v.tex:1344: Warning: Undefined label: 'SetStrictImplicit' >./RefMan-ext.v.tex:1344: Warning: Undefined label: 'SetContextualImplicit' >./RefMan-ext.v.tex:1344: Warning: Undefined label: 'SetReversiblePatternImplicit' >./RefMan-ext.v.tex:1345: Warning: Undefined label: 'SetMaximalImplicitInsertion' >./RefMan-ext.v.tex:1532: Warning: Undefined label: 'fig:explicitations' >./RefMan-ext.v.tex:1597: Warning: Undefined label: 'SetPrintingAll' >./RefMan-ext.v.tex:1786: Warning: Undefined label: 'Coercions-full' >./RefMan-ext.v.tex:1793: Warning: Undefined label: 'Addoc-syntax' >./RefMan-ext.v.tex:1820: Warning: Undefined label: 'Sorts' >./RefMan-ext.v.tex:1822: Warning: Undefined label: 'SetPrintingAll' >./RefMan-ext.v.tex:1833: Warning: Undefined label: 'Sorts' >./RefMan-lib.v.tex:15: Warning: Undefined label: 'Require' >./RefMan-lib.v.tex:21: Warning: Undefined label: 'Contributions' >./RefMan-lib.v.tex:48: Warning: Undefined label: 'init-notations' >./RefMan-lib.v.tex:119: Warning: Undefined label: 'formulas-syntax' >./RefMan-lib.v.tex:348: Warning: Undefined label: 'specif-syntax' >./RefMan-lib.v.tex:434: Warning: Undefined label: 'specif-syntax' >./RefMan-lib.v.tex:609: Warning: Undefined label: 'refine-example' >./RefMan-lib.v.tex:912: Warning: Undefined label: 'Other-commands' >./RefMan-lib.v.tex:921: Warning: Undefined label: 'zarith-syntax' >./RefMan-lib.v.tex:963: Warning: Undefined label: 'zarith-syntax' >./RefMan-lib.v.tex:991: Warning: Undefined label: 'nat-syntax' >./RefMan-lib.v.tex:1068: Warning: Undefined label: 'Tactics' >./RefMan-lib.v.tex:1151: Warning: Undefined label: 'TacticLanguage' >./RefMan-cic.v.tex:19: Warning: Undefined label: 'impredicativity' >./RefMan-cic.v.tex:31: Warning: Undefined label: 'Terms' >./RefMan-cic.v.tex:36: Warning: Undefined label: 'convertibility' >./RefMan-cic.v.tex:42: Warning: Undefined citation: 'GimCas05' >./RefMan-cic.v.tex:45: Warning: Undefined citation: 'CoqArt' >./RefMan-cic.v.tex:47: Warning: Undefined citation: 'Bar99' >./RefMan-cic.v.tex:47: Warning: Undefined citation: 'Wer94' >./RefMan-cic.v.tex:48: Warning: Undefined citation: 'Moh97' >./RefMan-cic.v.tex:49: Warning: Undefined citation: 'CoHu85a' >./RefMan-cic.v.tex:49: Warning: Undefined citation: 'CoHu85b' >./RefMan-cic.v.tex:49: Warning: Undefined citation: 'CoHu86' >./RefMan-cic.v.tex:50: Warning: Undefined citation: 'CoPa89' >./RefMan-cic.v.tex:53: Warning: Undefined citation: 'Bar91' >./RefMan-cic.v.tex:135: Warning: Undefined label: 'PrintingUniverses' >./RefMan-cic.v.tex:190: Warning: Undefined citation: 'Bar81' >./RefMan-cic.v.tex:269: Warning: Undefined label: 'Cic-inductive-definitions' >./RefMan-cic.v.tex:279: Warning: Undefined label: 'Cic-inductive-definitions' >./RefMan-cic.v.tex:349: Warning: Undefined label: 'conv-rules' >./RefMan-cic.v.tex:371: Warning: Undefined citation: 'Coq85' >./RefMan-cic.v.tex:375: Warning: Undefined label: 'iotared' >./RefMan-cic.v.tex:379: Warning: Undefined citation: 'Moh93' >./RefMan-cic.v.tex:379: Warning: Undefined citation: 'Wer94' >./RefMan-cic.v.tex:458: Warning: Undefined label: 'Tactics' >./RefMan-cic.v.tex:982: Warning: Undefined label: 'elimdep' >./RefMan-cic.v.tex:1024: Warning: Undefined label: 'singleton' >./RefMan-cic.v.tex:1026: Warning: Undefined label: 'impredicativity' >./RefMan-cic.v.tex:1033: Warning: Undefined label: 'elimdep' >./RefMan-cic.v.tex:1051: Warning: Undefined label: 'singleton' >./RefMan-cic.v.tex:1165: Warning: Undefined citation: 'Coq92' >./RefMan-cic.v.tex:1548: Warning: Undefined citation: 'Gim94' >./RefMan-cic.v.tex:1602: Warning: Undefined label: 'Fixpoint' >./RefMan-cic.v.tex:1773: Warning: Undefined label: 'Scheme' >./RefMan-cic.v.tex:1779: Warning: Undefined citation: 'Gimenez95b' >./RefMan-cic.v.tex:1779: Warning: Undefined citation: 'Gim98' >./RefMan-cic.v.tex:1779: Warning: Undefined citation: 'GimCas05' >./RefMan-modr.tex:47: Warning: Undefined label: 'Terms' >./RefMan-modr.tex:486: Warning: Undefined label: 'delta' >./RefMan-oth.v.tex:68: Warning: Undefined label: 'Conversion-tactics' >./RefMan-oth.v.tex:75: Warning: Undefined label: 'Sorts' >./RefMan-oth.v.tex:85: Warning: Undefined label: 'Extraction' >./RefMan-oth.v.tex:120: Warning: Undefined label: 'Require' >./RefMan-oth.v.tex:147: Warning: Undefined label: 'Notation' >./RefMan-oth.v.tex:154: Warning: Undefined label: 'scopechange' >./RefMan-oth.v.tex:372: Warning: Undefined label: 'LocateSymbol' >./RefMan-oth.v.tex:471: Warning: Undefined label: 'loadpath' >./RefMan-oth.v.tex:485: Warning: Undefined label: 'Begin-Silent' >./RefMan-oth.v.tex:495: Warning: Undefined label: 'Addoc-coqc' >./RefMan-oth.v.tex:519: Warning: Undefined label: 'loadpath' >./RefMan-oth.v.tex:528: Warning: Undefined label: 'Import' >./RefMan-oth.v.tex:569: Warning: Undefined label: 'loadpath' >./RefMan-oth.v.tex:596: Warning: Undefined label: 'Addoc-coqc' >./RefMan-oth.v.tex:611: Warning: Undefined label: 'loadpath' >./RefMan-oth.v.tex:614: Warning: Undefined label: 'Addoc-coqc' >./RefMan-oth.v.tex:625: Warning: Undefined label: 'Locate File' >./RefMan-oth.v.tex:632: Warning: Undefined label: 'LongNames' >./RefMan-oth.v.tex:706: Warning: Undefined label: 'compiled' >./RefMan-oth.v.tex:713: Warning: Undefined label: 'compiled' >./RefMan-oth.v.tex:722: Warning: Undefined label: 'compiled' >./RefMan-oth.v.tex:771: Warning: Undefined label: 'Proof-handling' >./RefMan-oth.v.tex:776: Warning: Undefined label: 'Proof-handling' >./RefMan-oth.v.tex:779: Warning: Undefined label: 'Proof-handling' >./RefMan-oth.v.tex:802: Warning: Undefined label: 'Proof-handling' >./RefMan-oth.v.tex:858: Warning: Undefined label: 'Pwd' >./RefMan-oth.v.tex:895: Warning: Undefined label: 'binary-images' >./RefMan-oth.v.tex:897: Warning: Undefined label: 'EnvVariables' >./RefMan-oth.v.tex:957: Warning: Undefined citation: 'Leroy90' >./RefMan-oth.v.tex:974: Warning: Undefined label: 'conv-rules' >./RefMan-oth.v.tex:981: Warning: Undefined label: 'Conversion-tactics' >./RefMan-oth.v.tex:981: Warning: Undefined label: 'Automatizing' >./RefMan-oth.v.tex:982: Warning: Undefined label: 'Theorem' >./RefMan-oth.v.tex:1017: Warning: Undefined label: 'Conversion-tactics' >./RefMan-oth.v.tex:1017: Warning: Undefined label: 'Automatizing' >./RefMan-oth.v.tex:1018: Warning: Undefined label: 'Theorem' >./RefMan-oth.v.tex:1068: Warning: Undefined label: 'vmcompute' >./RefMan-oth.v.tex:1068: Warning: Undefined label: 'vmoption' >./RefMan-pro.tex:5: Warning: Undefined label: 'Vernacular-commands' >./RefMan-pro.tex:10: Warning: Undefined label: 'Tactics' >./RefMan-pro.tex:24: Warning: Undefined label: 'intro' >./RefMan-pro.tex:30: Warning: Undefined citation: 'How80' >./RefMan-pro.tex:30: Warning: Undefined citation: 'Bar91' >./RefMan-pro.tex:30: Warning: Undefined citation: 'Gir89' >./RefMan-pro.tex:30: Warning: Undefined citation: 'Hue89' >./RefMan-pro.tex:35: Warning: Undefined label: 'Resume' >./RefMan-pro.tex:57: Warning: Undefined label: 'Theorem' >./RefMan-pro.tex:152: Warning: Undefined label: 'Defined' >./RefMan-pro.tex:167: Warning: Undefined label: 'exact' >./RefMan-pro.tex:176: Warning: Undefined label: 'ProofWith' >./RefMan-pro.tex:235: Warning: Undefined label: 'Show' >./RefMan-pro.tex:242: Warning: Undefined label: 'instantiate' >./RefMan-pro.tex:384: Warning: Undefined label: 'refine' >./RefMan-tac.v.tex:28: Warning: Undefined label: 'Show' >./RefMan-tac.v.tex:38: Warning: Undefined label: 'TacticLanguage' >./RefMan-tac.v.tex:68: Warning: Undefined label: 'conv-rules' >./RefMan-tac.v.tex:103: Warning: Undefined label: 'refine-example' >./RefMan-tac.v.tex:109: Warning: Undefined label: 'Cic' >./RefMan-tac.v.tex:116: Warning: Undefined label: 'Typed-terms' >./RefMan-tac.v.tex:250: Warning: Undefined label: 'Typed-terms' >./RefMan-tac.v.tex:298: Warning: Undefined label: 'LongNames' >./RefMan-tac.v.tex:308: Warning: Undefined label: 'intros-pattern' >./RefMan-tac.v.tex:361: Warning: Undefined label: 'move' >./RefMan-tac.v.tex:392: Warning: Undefined label: 'pattern' >./RefMan-tac.v.tex:402: Warning: Undefined label: 'pattern' >./RefMan-tac.v.tex:402: Warning: Undefined label: 'change' >./RefMan-tac.v.tex:432: Warning: Undefined label: 'Binding-list' >./RefMan-tac.v.tex:453: Warning: Undefined label: 'eapply-example' >./RefMan-tac.v.tex:513: Warning: Undefined label: 'Occurrences clauses' >./RefMan-tac.v.tex:593: Warning: Undefined label: 'Typed-terms' >./RefMan-tac.v.tex:606: Warning: Undefined label: 'intros-pattern' >./RefMan-tac.v.tex:637: Warning: Undefined label: 'Binding-list' >./RefMan-tac.v.tex:701: Warning: Undefined label: 'Binding-list' >./RefMan-tac.v.tex:819: Warning: Undefined label: 'Conv' >./RefMan-tac.v.tex:855: Warning: Undefined label: 'Conversion-tactics' >./RefMan-tac.v.tex:863: Warning: Undefined label: 'Tac-induction' >./RefMan-tac.v.tex:878: Warning: Undefined label: 'Guarded' >./RefMan-tac.v.tex:910: Warning: Undefined label: 'Guarded' >./RefMan-tac.v.tex:975: Warning: Undefined label: 'PrintAssumptions' >./RefMan-tac.v.tex:1005: Warning: Undefined label: 'elim' >./RefMan-tac.v.tex:1045: Warning: Undefined label: 'SetPrintingAll' >./RefMan-tac.v.tex:1047: Warning: Undefined label: 'Implicit Arguments' >./RefMan-tac.v.tex:1048: Warning: Undefined label: 'Coercions' >./RefMan-tac.v.tex:1074: Warning: Undefined label: 'tactic:set' >./RefMan-tac.v.tex:1074: Warning: Undefined label: 'Tac-induction' >./RefMan-tac.v.tex:1074: Warning: Undefined label: 'SetPrintingAll' >./RefMan-tac.v.tex:1144: Warning: Undefined label: 'tactic:set' >./RefMan-tac.v.tex:1144: Warning: Undefined label: 'rewrite' >./RefMan-tac.v.tex:1145: Warning: Undefined label: 'tactic:replace' >./RefMan-tac.v.tex:1146: Warning: Undefined label: 'tactic:autorewrite' >./RefMan-tac.v.tex:1182: Warning: Undefined label: 'Transparent' >./RefMan-tac.v.tex:1194: Warning: Undefined label: 'Opaque' >./RefMan-tac.v.tex:1287: Warning: Undefined label: 'Opaque' >./RefMan-tac.v.tex:1335: Warning: Undefined label: 'Simpl-definitions' >./RefMan-tac.v.tex:1335: Warning: Undefined label: 'Transparent' >./RefMan-tac.v.tex:1377: Warning: Undefined label: 'scopechange' >./RefMan-tac.v.tex:1551: Warning: Undefined label: 'eapply-example' >./RefMan-tac.v.tex:1560: Warning: Undefined label: 'Cic-inductive-definitions' >./RefMan-tac.v.tex:1647: Warning: Undefined label: 'intros-pattern' >./RefMan-tac.v.tex:1658: Warning: Undefined label: 'intros-pattern' >./RefMan-tac.v.tex:1668: Warning: Undefined label: 'Binding-list' >./RefMan-tac.v.tex:1676: Warning: Undefined label: 'eapply-example' >./RefMan-tac.v.tex:1700: Warning: Undefined label: 'Occurrences clauses' >./RefMan-tac.v.tex:1738: Warning: Undefined label: 'Binding-list' >./RefMan-tac.v.tex:1833: Warning: Undefined label: 'intros-pattern' >./RefMan-tac.v.tex:1851: Warning: Undefined label: 'intros-pattern' >./RefMan-tac.v.tex:1858: Warning: Undefined label: 'Binding-list' >./RefMan-tac.v.tex:1866: Warning: Undefined label: 'eapply-example' >./RefMan-tac.v.tex:1879: Warning: Undefined label: 'Occurrences clauses' >./RefMan-tac.v.tex:1976: Warning: Undefined label: 'intro' >./RefMan-tac.v.tex:1983: Warning: Undefined label: 'destruct' >./RefMan-tac.v.tex:2010: Warning: Undefined label: 'clear' >./RefMan-tac.v.tex:2168: Warning: Undefined citation: 'DBLP:conf/types/McBride00' >./RefMan-tac.v.tex:2169: Warning: Undefined citation: 'DBLP:conf/types/CornesT95' >./RefMan-tac.v.tex:2272: Warning: Undefined label: 'dependent-induction-example' >./RefMan-tac.v.tex:2306: Warning: Undefined label: 'Record' >./RefMan-tac.v.tex:2317: Warning: Undefined label: 'Function' >./RefMan-tac.v.tex:2318: Warning: Undefined label: 'FunScheme' >./RefMan-tac.v.tex:2358: Warning: Undefined label: 'Function' >./RefMan-tac.v.tex:2359: Warning: Undefined label: 'FunScheme' >./RefMan-tac.v.tex:2362: Warning: Undefined label: 'Function' >./RefMan-tac.v.tex:2366: Warning: Undefined label: 'Function' >./RefMan-tac.v.tex:2368: Warning: Undefined label: 'Function' >./RefMan-tac.v.tex:2371: Warning: Undefined label: 'Function' >./RefMan-tac.v.tex:2371: Warning: Undefined label: 'FunScheme' >./RefMan-tac.v.tex:2371: Warning: Undefined label: 'FunScheme-examples' >./RefMan-tac.v.tex:2372: Warning: Undefined label: 'sec:functional-inversion' >./RefMan-tac.v.tex:2387: Warning: Undefined label: 'Tac-induction' >./RefMan-tac.v.tex:2397: Warning: Undefined label: 'Tac-induction' >./RefMan-tac.v.tex:2401: Warning: Undefined label: 'Tac-induction' >./RefMan-tac.v.tex:2410: Warning: Undefined label: 'Equality' >./RefMan-tac.v.tex:2456: Warning: Undefined label: 'Conversion-tactics' >./RefMan-tac.v.tex:2479: Warning: Undefined label: 'pattern' >./RefMan-tac.v.tex:2561: Warning: Undefined label: 'Conversion-tactics' >./RefMan-tac.v.tex:2634: Warning: Undefined label: 'setoid_replace' >./RefMan-tac.v.tex:2836: Warning: Undefined label: 'Scheme' >./RefMan-tac.v.tex:3157: Warning: Undefined label: 'inversion-examples' >./RefMan-tac.v.tex:3193: Warning: Undefined label: 'inversion-examples' >./RefMan-tac.v.tex:3203: Warning: Undefined label: 'Function' >./RefMan-tac.v.tex:3239: Warning: Undefined label: 'quote-examples' >./RefMan-tac.v.tex:3294: Warning: Undefined label: 'Hints-databases' >./RefMan-tac.v.tex:3301: Warning: Undefined label: 'Hints-databases' >./RefMan-tac.v.tex:3323: Warning: Undefined label: 'Hints-databases' >./RefMan-tac.v.tex:3355: Warning: Undefined label: 'Hints-databases' >./RefMan-tac.v.tex:3382: Warning: Undefined citation: 'Dyc92' >./RefMan-tac.v.tex:3453: Warning: Undefined citation: 'Mun94' >./RefMan-tac.v.tex:3469: Warning: Undefined label: 'TacticLanguage' >./RefMan-tac.v.tex:3642: Warning: Undefined label: 'injection' >./RefMan-tac.v.tex:3642: Warning: Undefined label: 'discriminate' >./RefMan-tac.v.tex:3737: Warning: Undefined label: 'OmegaChapter' >./RefMan-tac.v.tex:3756: Warning: Undefined label: 'ring' >./RefMan-tac.v.tex:3782: Warning: Undefined label: 'ring' >./RefMan-tac.v.tex:3819: Warning: Undefined citation: 'Fourier' >./RefMan-tac.v.tex:3883: Warning: Undefined label: 'HintRewrite' >./RefMan-tac.v.tex:3885: Warning: Undefined label: 'autorewrite-example' >./RefMan-tac.v.tex:3901: Warning: Undefined label: 'PrintHint' >./RefMan-tac.v.tex:3921: Warning: Undefined label: 'HintTransparency' >./RefMan-tac.v.tex:3969: Warning: Undefined label: 'eauto' >./RefMan-tac.v.tex:4270: Warning: Undefined label: 'Section' >./RefMan-tac.v.tex:4321: Warning: Undefined label: 'BeginProof' >./RefMan-tac.v.tex:4418: Warning: Undefined label: 'Scheme-examples' >./RefMan-tac.v.tex:4449: Warning: Undefined label: 'CombinedScheme-examples' >./RefMan-tac.v.tex:4480: Warning: Undefined label: 'FunScheme-examples' >./RefMan-tac.v.tex:4503: Warning: Undefined label: 'Section' >./RefMan-tac.v.tex:4508: Warning: Undefined label: 'TacticLanguage' >./RefMan-ltac.v.tex:9: Warning: Undefined citation: 'Del00' >./RefMan-ltac.v.tex:9: Warning: Undefined label: 'Tactics-examples' >./RefMan-ltac.v.tex:29: Warning: Undefined label: 'ltac' >./RefMan-ltac.v.tex:30: Warning: Undefined label: 'ltac_aux' >./RefMan-ltac.v.tex:30: Warning: Undefined label: 'BNF-syntax' >./RefMan-ltac.v.tex:37: Warning: Undefined label: 'Tactics' >./RefMan-ltac.v.tex:56: Warning: Undefined label: 'ltactop' >./RefMan-ltac.v.tex:545: Warning: Undefined label: 'SetPrintingAll' >./RefMan-tacex.v.tex:471: Warning: Undefined label: 'FunInduction' >./RefMan-tacex.v.tex:510: Warning: Undefined label: 'Function' >./RefMan-tacex.v.tex:512: Warning: Undefined label: 'Function' >./RefMan-tacex.v.tex:1219: Warning: Undefined label: 'elim' >./RefMan-tacex.v.tex:1219: Warning: Undefined label: 'case' >./RefMan-tacex.v.tex:1219: Warning: Undefined label: 'inversion' >./RefMan-tacex.v.tex:1491: Warning: Undefined label: 'ring' >./RefMan-tacex.v.tex:1560: Warning: Undefined label: 'ring' >./RefMan-tacex.v.tex:1607: Warning: Undefined label: 'permutpred' >./RefMan-tacex.v.tex:1636: Warning: Undefined label: 'permutpred' >./RefMan-tacex.v.tex:1675: Warning: Undefined label: 'permutltac' >./RefMan-tacex.v.tex:1691: Warning: Undefined label: 'ltac' >./RefMan-tacex.v.tex:1808: Warning: Undefined citation: 'Dyc92' >./RefMan-tacex.v.tex:1809: Warning: Undefined label: 'tautoltaca' >./RefMan-tacex.v.tex:1810: Warning: Undefined label: 'tautoltacb' >./RefMan-tacex.v.tex:1845: Warning: Undefined citation: 'RC95' >./RefMan-tacex.v.tex:1846: Warning: Undefined label: 'isosax' >./RefMan-tacex.v.tex:1891: Warning: Undefined citation: 'RC95' >./RefMan-tacex.v.tex:1892: Warning: Undefined label: 'isosax' >./RefMan-tacex.v.tex:1982: Warning: Undefined label: 'isosltac1' >./RefMan-tacex.v.tex:1982: Warning: Undefined label: 'isosltac2' >./RefMan-decl.v.tex:129: Warning: Undefined label: 'lexical' >./RefMan-decl.v.tex:281: Warning: Undefined label: 'justifications' >./RefMan-decl.v.tex:1337: Warning: Undefined label: 'term-syntax-aux' >./RefMan-decl.v.tex:1492: Warning: Undefined citation: 'corbineau08types' >./RefMan-syn.v.tex:7: Warning: Undefined label: 'Notation' >./RefMan-syn.v.tex:10: Warning: Undefined label: 'scopes' >./RefMan-syn.v.tex:16: Warning: Undefined label: 'Abbreviations' >./RefMan-syn.v.tex:41: Warning: Undefined label: 'Abbreviations' >./RefMan-syn.v.tex:63: Warning: Undefined label: 'ReservedNotation' >./RefMan-syn.v.tex:128: Warning: Undefined label: 'init-notations' >./RefMan-syn.v.tex:223: Warning: Undefined label: 'Theories' >./RefMan-syn.v.tex:403: Warning: Undefined label: 'init-notations' >./RefMan-syn.v.tex:416: Warning: Undefined label: 'notation-syntax' >./RefMan-syn.v.tex:452: Warning: Undefined label: 'SetPrintingAll' >./RefMan-syn.v.tex:492: Warning: Undefined label: 'Locate' >./RefMan-syn.v.tex:600: Warning: Undefined label: 'scopes' >./RefMan-syn.v.tex:652: Warning: Undefined label: 'notation-syntax' >./RefMan-syn.v.tex:653: Warning: Undefined label: 'scopes' >./RefMan-syn.v.tex:697: Warning: Undefined label: 'notation-syntax' >./RefMan-syn.v.tex:813: Warning: Undefined label: 'About' >./RefMan-syn.v.tex:829: Warning: Undefined label: 'Coercions-full' >./RefMan-syn.v.tex:869: Warning: Undefined label: 'About' >./RefMan-syn.v.tex:965: Warning: Undefined label: 'strings' >./RefMan-com.tex:45: Warning: Undefined label: 'compiled' >./RefMan-com.tex:48: Warning: Undefined label: 'lexical' >./RefMan-com.tex:81: Warning: Undefined label: 'Makefile' >./RefMan-com.tex:107: Warning: Undefined label: 'LongNames' >./RefMan-com.tex:116: Warning: Undefined label: 'AddLoadPath' >./RefMan-com.tex:117: Warning: Undefined label: 'Libraries' >./RefMan-com.tex:126: Warning: Undefined label: 'AddRecLoadPath' >./RefMan-com.tex:127: Warning: Undefined label: 'Libraries' >./RefMan-com.tex:262: Warning: Undefined label: 'coqdoc' >./RefMan-com.tex:273: Warning: Undefined label: 'SetVirtualMachine' >./Helm.tex:24: Warning: Undefined label: 'Makefile' >./Helm.tex:74: Warning: Undefined label: 'coqdoc' >./Helm.tex:199: Warning: Undefined label: 'Section' >./RefMan-ide.tex:14: Warning: Undefined label: 'Addoc-coqc' >./RefMan-ide.tex:34: Warning: Undefined label: 'fig:coqide' >./RefMan-ide.tex:68: Warning: Undefined label: 'fig:coqide' >./RefMan-ide.tex:151: Warning: Undefined label: 'fig:querywindow' >./RefMan-ide.tex:182: Warning: Undefined label: 'sec:coqidecharencoding' >./RefMan-ide.tex:195: Warning: Undefined label: 'sec:trytactics' >./RefMan-ide.tex:225: Warning: Undefined label: 'Addoc-syntax' >./RefMan-ide.tex:310: Warning: Undefined label: 'Coqmktop' >./Cases.v.tex:14: Warning: Undefined label: 'term-syntax' >./Cases.v.tex:15: Warning: Undefined label: 'term-syntax-aux' >./Cases.v.tex:569: Warning: Undefined label: 'refine-example' >./Cases.v.tex:631: Warning: Undefined label: 'refine' >./Coercion.v.tex:41: Warning: Undefined label: 'fig:classes' >./Coercion.v.tex:206: Warning: Undefined label: 'sentences-syntax' >./Coercion.v.tex:227: Warning: Undefined label: 'sentences-syntax' >./Coercion.v.tex:330: Warning: Undefined label: 'Record' >./Classes.v.tex:17: Warning: Undefined citation: 'sozeau08' >./Classes.v.tex:48: Warning: \overrightarrow outside display mode >./Classes.v.tex:49: Warning: \overrightarrow outside display mode >./Classes.v.tex:163: Warning: Undefined label: 'classes:impl-quant' >./Classes.v.tex:164: Warning: Undefined label: 'classes:superclasses' >./Classes.v.tex:290: Warning: Undefined label: 'SingletonClass' >./Classes.v.tex:368: Warning: Undefined label: 'Program' >./Classes.v.tex:396: Warning: Undefined label: 'HintTransparency' >./Micromega.v.tex:5: Warning: Undefined label: 'sec:psatz-hurry' >./Micromega.v.tex:7: Warning: Undefined label: 'sec:psatz-back' >./Micromega.v.tex:9: Warning: Undefined label: 'sec:lia' >./Micromega.v.tex:86: Warning: Undefined label: 'ring' >./Micromega.v.tex:98: Warning: Undefined label: 'thm:psatz' >./Micromega.v.tex:123: Warning: Undefined label: 'OmegaChapter' >./Micromega.v.tex:124: Warning: Undefined citation: 'TheOmegaPaper' >./Extraction.v.tex:185: Warning: Undefined label: 'extraction:axioms' >./Extraction.v.tex:391: Warning: Undefined citation: 'Let02' >./Extraction.v.tex:764: Warning: Undefined citation: 'Let02' >./Program.v.tex:12: Warning: Undefined citation: 'Sozeau06' >./Program.v.tex:13: Warning: Undefined label: 'Extraction' >./Program.v.tex:17: Warning: Undefined citation: 'Rushby98' >./Program.v.tex:21: Warning: Undefined citation: 'Parent95b' >./Program.v.tex:43: Warning: Undefined label: 'Caseexpr' >./Program.v.tex:84: Warning: Undefined label: 'Simpl-definitions' >./Program.v.tex:84: Warning: Undefined label: 'Fixpoint' >./Program.v.tex:124: Warning: Undefined label: 'Opaque' >./Program.v.tex:124: Warning: Undefined label: 'Transparent' >./Program.v.tex:124: Warning: Undefined label: 'unfold' >./Program.v.tex:131: Warning: Undefined label: 'Fixpoint' >./Polynom.v.tex:205: Warning: Undefined label: 'setoidtactics' >./Polynom.v.tex:374: Warning: Undefined label: 'setoidtactics' >./Polynom.v.tex:611: Warning: Undefined label: 'setoidtactics' >./Polynom.v.tex:901: Warning: Undefined label: 'ring' >./Polynom.v.tex:906: Warning: Undefined label: 'ring' >./Polynom.v.tex:928: Warning: Undefined citation: 'DelMay01' >./Polynom.v.tex:963: Warning: Undefined citation: 'Bou97' >./Polynom.v.tex:969: Warning: Undefined label: 'DiscussReflection' >./Setoid.v.tex:143: Warning: Undefined label: 'setoidtactics' >./Setoid.v.tex:333: Warning: Undefined label: 'setoid:first-class' >./Setoid.v.tex:474: Warning: Undefined label: 'typeclasses' >./Setoid.v.tex:716: Warning: Undefined label: 'TypeclassesTransparency' >./Reference-Manual.bbl:122: Warning: Undefined citation: 'DBLP:conf/types/2002' >./Reference-Manual.bbl:146: Warning: Undefined citation: 'CoC89' >./Reference-Manual.bbl:157: Warning: Undefined citation: 'Bastad92' >./Reference-Manual.bbl:162: Warning: Undefined citation: 'Nijmegen93' >./Reference-Manual.bbl:206: Warning: Undefined citation: 'DBLP:conf/types/1995' >./Reference-Manual.bbl:358: Warning: Undefined citation: 'Filliatre99' >./Reference-Manual.bbl:464: Warning: Undefined citation: 'Hue87tapsoft' >./Reference-Manual.bbl:477: Warning: Undefined citation: 'CoC89' >./Reference-Manual.bbl:545: Warning: Undefined citation: 'DBLP:conf/types/2002' >./Reference-Manual.bbl:578: Warning: Undefined citation: 'DBLP:conf/types/2000' >./Reference-Manual.bbl:603: Warning: Undefined citation: 'DBLP:conf/types/2002' >./Reference-Manual.bbl:653: Warning: Undefined citation: 'Nijmegen93' >HeVeA Warning: Label(s) may have changed. Rerun me to get cross-references right. >Run, run, again... >Exclude comment 'comment' >./Classes.v.tex:48: Warning: \overrightarrow outside display mode >./Classes.v.tex:49: Warning: \overrightarrow outside display mode >Fixpoint reached in 2 step(s) >install -m 644 doc/common/styles/html/simple/cover.html doc/refman >rm -rf doc/refman/html >install -d doc/refman/html >install -m 644 doc/refman/coqide.png doc/refman/coqide-queries.png doc/refman/html >(cd doc/refman/html; hacha -nolinks -tocbis -o toc.html ../styles.hva ../Reference-Manual.html) >install -m 644 doc/refman/cover.html doc/refman/html/index.html >install -m 644 doc/common/styles/html/simple/*.css doc/refman/html >(cd `dirname doc/refman/Reference-Manual.dvi`; dvips -q -o `basename doc/refman/Reference-Manual.ps` `basename doc/refman/Reference-Manual.dvi`) >(cd doc/refman;\ > pdflatex -interaction=batchmode Reference-Manual.tex;\ > ../tools/show_latex_messages -no-overfull Reference-Manual.log) >This is pdfTeXk, Version 3.1415926-1.40.9 (Web2C 7.5.7) > %&-line parsing enabled. >entering extended mode >(cd `dirname doc/faq/FAQ.tex`; /var/tmp/portage/sci-mathematics/coq-8.2_p1-r1/work/coq-8.2pl1/bin/coq-tex -n 72 -image "/var/tmp/portage/sci-mathematics/coq-8.2_p1-r1/work/coq-8.2pl1/bin/coqtop -boot" -sl -small `basename doc/faq/FAQ.tex`) >Your version of coqtop seems OK >(cd doc/faq;\ > latex -interaction=batchmode FAQ.v;\ > BIBINPUTS=.: bibtex -min-crossrefs=10 -terse FAQ.v;\ > latex -interaction=batchmode FAQ.v > /dev/null;\ > latex -interaction=batchmode FAQ.v > /dev/null;\ > ../tools/show_latex_messages FAQ.v.log) >This is pdfTeXk, Version 3.1415926-1.40.9 (Web2C 7.5.7) > %&-line parsing enabled. >entering extended mode >LaTeX Font Warning: Font shape `OT1/cmr/bx/sc' undefined >LaTeX Font Warning: Font shape `OMS/cmtt/m/n' undefined >Overfull \hbox (15.0pt too wide) in paragraph at lines 515--518 (file FAQ.v.tex) >LaTeX Font Warning: Font shape `OMS/cmtt/m/it' undefined >Overfull \hbox (2.0598pt too wide) in paragraph at lines 3443--3447 (file FAQ.v.tex) >LaTeX Font Warning: Font shape `OMS/cmtt/bx/n' undefined >LaTeX Font Warning: Some font shapes were not available, defaults substituted. >(cd doc/faq; hevea -fix -exec xxdate.exe FAQ.v.tex) >Exclude comment 'comment' >./FAQ.v.tex:141: Warning: Undefined label: 'lastquestion' >./FAQ.v.tex:155: Warning: File \jobname.htoc not found >./FAQ.v.tex:250: Warning: Undefined citation: 'ProofsTypes' >./FAQ.v.tex:251: Warning: Undefined citation: 'Types:Dowek' >./FAQ.v.tex:253: Warning: Undefined citation: 'Pau96b' >./FAQ.v.tex:255: Warning: Undefined citation: 'EGThese' >./FAQ.v.tex:365: Warning: Undefined citation: 'Coq:manual' >./FAQ.v.tex:366: Warning: Undefined citation: 'Coq:Tutorial' >./FAQ.v.tex:385: Warning: Undefined label: 'coqbug' >./FAQ.v.tex:410: Warning: Undefined citation: 'Coq:manual' >./FAQ.v.tex:411: Warning: Undefined citation: 'Coq:coqart' >./FAQ.v.tex:449: Warning: Undefined citation: 'CoHu86' >./FAQ.v.tex:450: Warning: Undefined citation: 'Luo90' >./FAQ.v.tex:451: Warning: Undefined citation: 'CoPa89' >./FAQ.v.tex:541: Warning: Undefined citation: 'HofStr98' >./FAQ.v.tex:556: Warning: Undefined label: 'proof-irrelevance' >./FAQ.v.tex:558: Warning: Undefined citation: 'HofStr98' >./FAQ.v.tex:566: Warning: Undefined citation: 'HofStr98' >./FAQ.v.tex:708: Warning: Undefined label: 'proof-irrelevance' >./FAQ.v.tex:714: Warning: Undefined label: 'le-uniqueness' >./FAQ.v.tex:726: Warning: Undefined citation: 'HofStr98' >./FAQ.v.tex:727: Warning: Undefined label: 'proof-irrelevance' >./FAQ.v.tex:792: Warning: Undefined citation: 'Gir70' >./FAQ.v.tex:792: Warning: Undefined citation: 'Coq85' >./FAQ.v.tex:2147: Warning: Undefined label: 'opaque' >./FAQ.v.tex:2440: Warning: Undefined label: 'implicit' >./FAQ.v.tex:2764: Warning: Undefined citation: 'coqart' >./FAQ.v.tex:2767: Warning: Undefined label: 'minmax' >./FAQ.v.tex:3162: Warning: Undefined label: 'forallcoqide' >./FAQ.v.tex:3381: Warning: Undefined label: 'K-nat' >./FAQ.v.tex:3681: Warning: Undefined label: 'inputmeth' >./FAQ.v.tex:3813: Warning: Undefined citation: 'howe' >./FAQ.v.tex:3813: Warning: Undefined citation: 'harrison' >./FAQ.v.tex:3813: Warning: Undefined citation: 'boutin' >./FAQ.v.tex:3823: Warning: Undefined label: 'proof-irrelevance' >./FAQ.v.tex:3961: Warning: Undefined citation: 'Coq:manual' >./FAQ.v.tex:3962: Warning: Undefined citation: 'Coq:coqart' >./FAQ.v.tex:3965: Warning: Undefined citation: 'Coq:Tutorial' >********************************************* >********* That makes 176 questions ********** >********************************************* >HeVeA Warning: Label(s) may have changed. Rerun me to get cross-references right. >Run, run, again... >Exclude comment 'comment' >./FAQ.v.htoc:20: Warning: List with no item >./FAQ.v.htoc:34: Warning: List with no item >./FAQ.v.htoc:42: Warning: List with no item >./FAQ.v.htoc:192: Warning: List with no item >./FAQ.v.htoc:206: Warning: List with no item >./FAQ.v.htoc:212: Warning: List with no item >./FAQ.v.htoc:225: Warning: List with no item >./FAQ.v.htoc:237: Warning: List with no item >./FAQ.v.htoc:251: Warning: List with no item >./FAQ.v.htoc:259: Warning: List with no item >./FAQ.v.htoc:274: Warning: List with no item >./FAQ.v.htoc:287: Warning: List with no item >./FAQ.v.htoc:293: Warning: List with no item >********************************************* >********* That makes 176 questions ********** >********************************************* >Fixpoint reached in 2 step(s) >rm -rf doc/faq/html >install -d doc/faq/html >install -m 644 doc/faq/interval_discr.v doc/faq/axioms.png doc/faq/html >install -m 644 doc/faq/FAQ.v.html doc/faq/html/index.html >(cd `dirname doc/faq/FAQ.v.dvi`; dvips -q -o `basename doc/faq/FAQ.v.ps` `basename doc/faq/FAQ.v.dvi`) >(cd doc/faq;\ > pdflatex -interaction=batchmode FAQ.v.tex;\ > ../tools/show_latex_messages FAQ.v.log) >This is pdfTeXk, Version 3.1415926-1.40.9 (Web2C 7.5.7) > %&-line parsing enabled. >entering extended mode >LaTeX Font Warning: Font shape `OT1/cmr/bx/sc' undefined >LaTeX Font Warning: Font shape `OMS/cmtt/m/n' undefined >Overfull \hbox (15.0pt too wide) in paragraph at lines 513--518 (file FAQ.v.tex) >LaTeX Font Warning: Font shape `OMS/cmtt/m/it' undefined >Overfull \hbox (2.0598pt too wide) in paragraph at lines 3443--3447 (file FAQ.v.tex) >LaTeX Font Warning: Font shape `OMS/cmtt/bx/n' undefined >LaTeX Font Warning: Some font shapes were not available, defaults substituted. >(cd `dirname doc/tutorial/Tutorial.tex`; /var/tmp/portage/sci-mathematics/coq-8.2_p1-r1/work/coq-8.2pl1/bin/coq-tex -n 72 -image "/var/tmp/portage/sci-mathematics/coq-8.2_p1-r1/work/coq-8.2pl1/bin/coqtop -boot" -sl -small `basename doc/tutorial/Tutorial.tex`) >Your version of coqtop seems OK >(cd doc/tutorial; hevea -fix -exec xxdate.exe Tutorial.v) >../common/macros.tex:208: Warning: Defining '\proof' by \renewcommand >./Tutorial.v.tex:13: Warning: Command not found: \vfill >./Tutorial.v.tex:13: Warning: \hbox >./Tutorial.v.tex:13: Warning: Command not found: \vfill >HeVeA Warning: Label(s) may have changed. Rerun me to get cross-references right. >Run, run, again... >../common/macros.tex:208: Warning: Defining '\proof' by \renewcommand >./Tutorial.v.tex:13: Warning: Command not found: \vfill >./Tutorial.v.tex:13: Warning: \hbox >./Tutorial.v.tex:13: Warning: Command not found: \vfill >Fixpoint reached in 2 step(s) >(cd doc/tutorial;\ > latex -interaction=batchmode Tutorial.v;\ > ../tools/show_latex_messages Tutorial.v.log) >This is pdfTeXk, Version 3.1415926-1.40.9 (Web2C 7.5.7) > %&-line parsing enabled. >entering extended mode >Overfull \hbox (5.22331pt too wide) in paragraph at lines 196--200 (file Tutorial.v.tex) >Overfull \hbox (2.92325pt too wide) in paragraph at lines 256--265 (file Tutorial.v.tex) >Overfull \hbox (60.87pt too wide) in paragraph at lines 872--872 (file Tutorial.v.tex) >Overfull \hbox (64.2545pt too wide) in paragraph at lines 877--891 (file Tutorial.v.tex) >Overfull \hbox (48.0pt too wide) in paragraph at lines 1087--1087 (file Tutorial.v.tex) >Overfull \hbox (7.19824pt too wide) in paragraph at lines 1155--1155 (file Tutorial.v.tex) >Overfull \hbox (51.49773pt too wide) in paragraph at lines 1195--1204 (file Tutorial.v.tex) >Overfull \hbox (48.0pt too wide) in paragraph at lines 1457--1457 (file Tutorial.v.tex) >Overfull \hbox (48.0pt too wide) in paragraph at lines 1459--1459 (file Tutorial.v.tex) >Overfull \hbox (12.29822pt too wide) in paragraph at lines 1466--1466 (file Tutorial.v.tex) >Overfull \hbox (48.0pt too wide) in paragraph at lines 1480--1480 (file Tutorial.v.tex) >Overfull \hbox (48.0pt too wide) in paragraph at lines 1503--1503 (file Tutorial.v.tex) >Overfull \hbox (60.0pt too wide) in paragraph at lines 1520--1520 (file Tutorial.v.tex) >Overfull \hbox (48.0pt too wide) in paragraph at lines 1586--1586 (file Tutorial.v.tex) >Overfull \hbox (36.0pt too wide) in paragraph at lines 1592--1592 (file Tutorial.v.tex) >Overfull \hbox (30.54993pt too wide) in paragraph at lines 1677--1677 (file Tutorial.v.tex) >Overfull \hbox (27.59814pt too wide) in paragraph at lines 1942--1942 (file Tutorial.v.tex) >Overfull \hbox (6.0pt too wide) in paragraph at lines 1994--1994 (file Tutorial.v.tex) >Overfull \hbox (6.0pt too wide) in paragraph at lines 2042--2042 (file Tutorial.v.tex) >Overfull \hbox (96.0pt too wide) in paragraph at lines 2056--2056 (file Tutorial.v.tex) >Overfull \hbox (78.24998pt too wide) in paragraph at lines 2190--2190 (file Tutorial.v.tex) >Overfull \hbox (72.24998pt too wide) in paragraph at lines 2194--2194 (file Tutorial.v.tex) >Overfull \hbox (78.24998pt too wide) in paragraph at lines 2198--2198 (file Tutorial.v.tex) >Overfull \hbox (24.76382pt too wide) in paragraph at lines 2279--2283 (file Tutorial.v.tex) >Overfull \hbox (41.43161pt too wide) has occurred while \output is active (file Tutorial.v.tex) >Overfull \hbox (54.0pt too wide) in paragraph at lines 2329--2329 (file Tutorial.v.tex) >Overfull \hbox (54.0pt too wide) in paragraph at lines 2334--2334 (file Tutorial.v.tex) >Overfull \hbox (120.0pt too wide) in paragraph at lines 2355--2355 (file Tutorial.v.tex) >Overfull \hbox (27.59814pt too wide) in paragraph at lines 2369--2369 (file Tutorial.v.tex) >Overfull \hbox (32.69812pt too wide) in paragraph at lines 2379--2379 (file Tutorial.v.tex) >Overfull \hbox (41.43161pt too wide) has occurred while \output is active (file Tutorial.v.tex) >Overfull \hbox (41.43161pt too wide) has occurred while \output is active (file Tutorial.v.tex) >Overfull \hbox (42.0pt too wide) in paragraph at lines 2770--2770 (file Tutorial.v.tex) >Overfull \hbox (54.0pt too wide) in paragraph at lines 2787--2787 (file Tutorial.v.tex) >Overfull \hbox (0.65755pt too wide) in paragraph at lines 2912--2919 (file Tutorial.v.tex) >Overfull \hbox (0.14989pt too wide) in paragraph at lines 2968--2968 (file Tutorial.v.tex) >Overfull \hbox (18.0pt too wide) in paragraph at lines 2979--2979 (file Tutorial.v.tex) >Overfull \hbox (96.0pt too wide) in paragraph at lines 2980--2980 (file Tutorial.v.tex) >(cd `dirname doc/tutorial/Tutorial.v.dvi`; dvips -q -o `basename doc/tutorial/Tutorial.v.ps` `basename doc/tutorial/Tutorial.v.dvi`) >(cd doc/tutorial;\ > pdflatex -interaction=batchmode Tutorial.v.tex;\ > ../tools/show_latex_messages Tutorial.v.log) >This is pdfTeXk, Version 3.1415926-1.40.9 (Web2C 7.5.7) > %&-line parsing enabled. >entering extended mode >Overfull \hbox (5.22331pt too wide) in paragraph at lines 196--200 (file Tutorial.v.tex) >Overfull \hbox (2.92325pt too wide) in paragraph at lines 256--265 (file Tutorial.v.tex) >Overfull \hbox (60.87pt too wide) in paragraph at lines 872--872 (file Tutorial.v.tex) >Overfull \hbox (64.2545pt too wide) in paragraph at lines 877--891 (file Tutorial.v.tex) >Overfull \hbox (48.0pt too wide) in paragraph at lines 1087--1087 (file Tutorial.v.tex) >Overfull \hbox (7.19824pt too wide) in paragraph at lines 1155--1155 (file Tutorial.v.tex) >Overfull \hbox (51.49773pt too wide) in paragraph at lines 1195--1204 (file Tutorial.v.tex) >Overfull \hbox (48.0pt too wide) in paragraph at lines 1457--1457 (file Tutorial.v.tex) >Overfull \hbox (48.0pt too wide) in paragraph at lines 1459--1459 (file Tutorial.v.tex) >Overfull \hbox (12.29822pt too wide) in paragraph at lines 1466--1466 (file Tutorial.v.tex) >Overfull \hbox (48.0pt too wide) in paragraph at lines 1480--1480 (file Tutorial.v.tex) >Overfull \hbox (48.0pt too wide) in paragraph at lines 1503--1503 (file Tutorial.v.tex) >Overfull \hbox (60.0pt too wide) in paragraph at lines 1520--1520 (file Tutorial.v.tex) >Overfull \hbox (48.0pt too wide) in paragraph at lines 1586--1586 (file Tutorial.v.tex) >Overfull \hbox (36.0pt too wide) in paragraph at lines 1592--1592 (file Tutorial.v.tex) >Overfull \hbox (30.54993pt too wide) in paragraph at lines 1677--1677 (file Tutorial.v.tex) >Overfull \hbox (27.59814pt too wide) in paragraph at lines 1942--1942 (file Tutorial.v.tex) >Overfull \hbox (6.0pt too wide) in paragraph at lines 1994--1994 (file Tutorial.v.tex) >Overfull \hbox (6.0pt too wide) in paragraph at lines 2042--2042 (file Tutorial.v.tex) >Overfull \hbox (96.0pt too wide) in paragraph at lines 2056--2056 (file Tutorial.v.tex) >Overfull \hbox (78.24998pt too wide) in paragraph at lines 2190--2190 (file Tutorial.v.tex) >Overfull \hbox (72.24998pt too wide) in paragraph at lines 2194--2194 (file Tutorial.v.tex) >Overfull \hbox (78.24998pt too wide) in paragraph at lines 2198--2198 (file Tutorial.v.tex) >Overfull \hbox (24.76382pt too wide) in paragraph at lines 2279--2283 (file Tutorial.v.tex) >Overfull \hbox (41.43161pt too wide) has occurred while \output is active (file Tutorial.v.tex) >Overfull \hbox (54.0pt too wide) in paragraph at lines 2329--2329 (file Tutorial.v.tex) >Overfull \hbox (54.0pt too wide) in paragraph at lines 2334--2334 (file Tutorial.v.tex) >Overfull \hbox (120.0pt too wide) in paragraph at lines 2355--2355 (file Tutorial.v.tex) >Overfull \hbox (27.59814pt too wide) in paragraph at lines 2369--2369 (file Tutorial.v.tex) >Overfull \hbox (32.69812pt too wide) in paragraph at lines 2379--2379 (file Tutorial.v.tex) >Overfull \hbox (41.43161pt too wide) has occurred while \output is active (file Tutorial.v.tex) >Overfull \hbox (41.43161pt too wide) has occurred while \output is active (file Tutorial.v.tex) >Overfull \hbox (42.0pt too wide) in paragraph at lines 2770--2770 (file Tutorial.v.tex) >Overfull \hbox (54.0pt too wide) in paragraph at lines 2787--2787 (file Tutorial.v.tex) >Overfull \hbox (0.65755pt too wide) in paragraph at lines 2912--2919 (file Tutorial.v.tex) >Overfull \hbox (0.14989pt too wide) in paragraph at lines 2968--2968 (file Tutorial.v.tex) >Overfull \hbox (18.0pt too wide) in paragraph at lines 2979--2979 (file Tutorial.v.tex) >Overfull \hbox (96.0pt too wide) in paragraph at lines 2980--2980 (file Tutorial.v.tex) >(cd doc/RecTutorial; hevea -fix -exec xxdate.exe RecTutorial) >./RecTutorial.tex:42: Warning: Defining '\familydefault' by \renewcommand >./RecTutorial.tex:43: Warning: Defining '\seriesdefault' by \renewcommand >./RecTutorial.tex:44: Warning: Defining '\shapedefault' by \renewcommand >./RecTutorial.tex:67: Warning: File \jobname.htoc not found >./RecTutorial.tex:81: Warning: Undefined citation: 'Coquand:metamathematical' >./RecTutorial.tex:82: Warning: Undefined citation: 'coqrefman' >./RecTutorial.tex:84: Warning: Undefined citation: 'coqsite' >./RecTutorial.tex:85: Warning: Undefined citation: 'coqart' >./RecTutorial.tex:86: Warning: Undefined citation: 'Booksite' >./RecTutorial.tex:90: Warning: Undefined citation: 'coqrefman' >./RecTutorial.tex:110: Warning: Undefined label: 'CaseAnalysis' >./RecTutorial.tex:116: Warning: Undefined label: 'Introduction' >./RecTutorial.tex:116: Warning: Undefined label: 'CaseTechniques' >./RecTutorial.tex:118: Warning: Undefined label: 'StructuralInduction' >./RecTutorial.tex:120: Warning: Undefined label: 'CaseStudy' >./RecTutorial.tex:122: Warning: Undefined label: 'CoInduction' >./RecTutorial.tex:212: Warning: Undefined label: 'StructuralInduction' >./RecTutorial.tex:230: Warning: Undefined citation: 'coqrefman' >./RecTutorial.tex:398: Warning: Undefined label: 'vectors' >./RecTutorial.tex:528: Warning: Undefined label: 'WellFoundedRecursion' >./RecTutorial.tex:574: Warning: Undefined citation: 'coqrefman' >./RecTutorial.tex:574: Warning: Undefined citation: 'coqart' >./RecTutorial.tex:707: Warning: Undefined label: 'WellFoundedRecursion' >./RecTutorial.tex:880: Warning: Command not found: \boldsymbol >./RecTutorial.tex:880: Warning: Command not found: \boldsymbol >./RecTutorial.tex:900: Warning: Undefined label: 'inversion' >./RecTutorial.tex:904: Warning: Undefined label: 'firstpred' >./RecTutorial.tex:1382: Warning: Undefined label: 'CaseScheme' >./RecTutorial.tex:1582: Warning: Undefined label: 'ex-def' >./RecTutorial.tex:1586: Warning: Undefined citation: 'coqart' >./RecTutorial.tex:1641: Warning: Undefined label: 'MutuallyDependent' >./RecTutorial.tex:1686: Warning: Undefined citation: 'Bar98' >./RecTutorial.tex:1686: Warning: Undefined citation: 'Coq86' >./RecTutorial.tex:1770: Warning: Undefined citation: 'Coq86' >./RecTutorial.tex:1838: Warning: Undefined label: 'Discrimination' >./RecTutorial.tex:1893: Warning: Defining '\multirowsetup' by \renewcommand >./RecTutorial.tex:1897: Warning: Command not found: \multirow >./RecTutorial.tex:1897: Warning: Command not found: \LL >./RecTutorial.tex:1901: Warning: \cline changed into \hline >./RecTutorial.tex:1903: Warning: \cline changed into \hline >./RecTutorial.tex:1905: Warning: \cline changed into \hline >./RecTutorial.tex:1923: Warning: Undefined label: 'Introduction' >./RecTutorial.tex:1937: Warning: Undefined label: 'Introduction' >./RecTutorial.tex:2084: Warning: Undefined label: 'DependentCase' >./RecTutorial.tex:2106: Warning: Undefined label: 'Introduction' >./RecTutorial.tex:2703: Warning: Undefined label: 'natdoublerect' >./RecTutorial.tex:2826: Warning: Undefined label: 'parameterstuff' >./RecTutorial.tex:2857: Warning: Undefined label: 'parameterstuff' >./RecTutorial.tex:3075: Warning: Undefined label: 'vectors' >./RecTutorial.tex:3121: Warning: Undefined citation: 'conor:motive' >./RecTutorial.tex:3154: Warning: Undefined citation: 'coqart' >./RecTutorial.tex:3344: Warning: Undefined citation: 'EG96' >./RecTutorial.tex:3344: Warning: Undefined citation: 'EG95a' >./RecTutorial.tex:3365: Warning: Undefined citation: 'coqart' >./RecTutorial.tex:3398: Warning: Undefined citation: 'EG94a' >./RecTutorial.tex:3449: Warning: Undefined citation: 'EG95a' >./RecTutorial.tex:3530: Warning: Undefined label: 'WellFoundedRecursion' >./RecTutorial.tex:3575: Warning: Undefined label: 'zeroton' >./RecTutorial.tex:3580: Warning: Undefined label: 'CaseTechniques' >HeVeA Warning: Label(s) may have changed. Rerun me to get cross-references right. >Run, run, again... >./RecTutorial.tex:42: Warning: Defining '\familydefault' by \renewcommand >./RecTutorial.tex:43: Warning: Defining '\seriesdefault' by \renewcommand >./RecTutorial.tex:44: Warning: Defining '\shapedefault' by \renewcommand >./RecTutorial.tex:81: Warning: Undefined citation: 'Coquand:metamathematical' >./RecTutorial.tex:82: Warning: Undefined citation: 'coqrefman' >./RecTutorial.tex:84: Warning: Undefined citation: 'coqsite' >./RecTutorial.tex:85: Warning: Undefined citation: 'coqart' >./RecTutorial.tex:86: Warning: Undefined citation: 'Booksite' >./RecTutorial.tex:90: Warning: Undefined citation: 'coqrefman' >./RecTutorial.tex:230: Warning: Undefined citation: 'coqrefman' >./RecTutorial.tex:574: Warning: Undefined citation: 'coqrefman' >./RecTutorial.tex:574: Warning: Undefined citation: 'coqart' >./RecTutorial.tex:880: Warning: Command not found: \boldsymbol >./RecTutorial.tex:880: Warning: Command not found: \boldsymbol >./RecTutorial.tex:1586: Warning: Undefined citation: 'coqart' >./RecTutorial.tex:1686: Warning: Undefined citation: 'Bar98' >./RecTutorial.tex:1686: Warning: Undefined citation: 'Coq86' >./RecTutorial.tex:1770: Warning: Undefined citation: 'Coq86' >./RecTutorial.tex:1893: Warning: Defining '\multirowsetup' by \renewcommand >./RecTutorial.tex:1897: Warning: Command not found: \multirow >./RecTutorial.tex:1897: Warning: Command not found: \LL >./RecTutorial.tex:1901: Warning: \cline changed into \hline >./RecTutorial.tex:1903: Warning: \cline changed into \hline >./RecTutorial.tex:1905: Warning: \cline changed into \hline >./RecTutorial.tex:3121: Warning: Undefined citation: 'conor:motive' >./RecTutorial.tex:3154: Warning: Undefined citation: 'coqart' >./RecTutorial.tex:3344: Warning: Undefined citation: 'EG96' >./RecTutorial.tex:3344: Warning: Undefined citation: 'EG95a' >./RecTutorial.tex:3365: Warning: Undefined citation: 'coqart' >./RecTutorial.tex:3398: Warning: Undefined citation: 'EG94a' >./RecTutorial.tex:3449: Warning: Undefined citation: 'EG95a' >Fixpoint reached in 2 step(s) >(cd doc/RecTutorial;\ > latex -interaction=batchmode RecTutorial;\ > BIBINPUTS=.: bibtex -min-crossrefs=10 -terse RecTutorial;\ > latex -interaction=batchmode RecTutorial > /dev/null;\ > latex -interaction=batchmode RecTutorial > /dev/null;\ > ../tools/show_latex_messages RecTutorial.log) >This is pdfTeXk, Version 3.1415926-1.40.9 (Web2C 7.5.7) > %&-line parsing enabled. >entering extended mode >I couldn't open file name `RecTutorial.aux' >! LaTeX Error: File `epic.sty' not found. (file RecTutorial.tex) > >Type X to quit or <RETURN> to proceed, >or enter new name. (Default extension: sty) > >Enter file name: >! Emergency stop. (file RecTutorial.tex) ><read *> > >l.33 \usepackage >{eepic}^^M >RecTutorial.haux RecTutorial.html RecTutorial.htoc RecTutorial.log RecTutorial.tex RecTutorial.v coqartmacros.tex manbiblio.bib morebib.bib recmacros.tex (cannot \read from terminal in nonstop modes) > > >Here is how much of TeX's memory you used: >1972 strings out of 50070 >21380 string characters out of 433056 >69326 words of memory out of 1100000 >5153 multiletter control sequences out of 10000+15000 >4709 words of font info for 16 fonts, out of 400000 for 5000 >28 hyphenation exceptions out of 8191 >32i,0n,24p,223b,37s stack positions out of 1500i,500n,1500p,200000b,5000s >No pages of output. > >make[1]: *** [doc/RecTutorial/RecTutorial.dvi] Error 1 >make[1]: Leaving directory `/var/tmp/portage/sci-mathematics/coq-8.2_p1-r1/work/coq-8.2pl1' >make: *** [world] Error 2 > [31;01m*[0m > [31;01m*[0m ERROR: sci-mathematics/coq-8.2_p1-r1 failed. > [31;01m*[0m Call stack: > [31;01m*[0m ebuild.sh, line 49: Called src_compile > [31;01m*[0m environment, line 2320: Called die > [31;01m*[0m The specific snippet of code: > [31;01m*[0m emake STRIP="true" -j1 || die "make failed" > [31;01m*[0m The die message: > [31;01m*[0m make failed > [31;01m*[0m > [31;01m*[0m If you need support, post the topmost build error, and the call stack if relevant. > [31;01m*[0m A complete build log is located at '/var/tmp/portage/sci-mathematics/coq-8.2_p1-r1/temp/build.log'. > [31;01m*[0m The ebuild environment file is located at '/var/tmp/portage/sci-mathematics/coq-8.2_p1-r1/temp/environment'. > [31;01m*[0m
You cannot view the attachment while viewing its details because your browser does not support IFRAMEs.
View the attachment on a separate page
.
View Attachment As Raw
Actions:
View
Attachments on
bug 292630
: 209799