>>> 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 to proceed, or enter new name. (Default extension: sty) Enter file name: ! Emergency stop. (file RecTutorial.tex) 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 * * ERROR: sci-mathematics/coq-8.2_p1-r1 failed. * Call stack: * ebuild.sh, line 49: Called src_compile * environment, line 2320: Called die * The specific snippet of code: * emake STRIP="true" -j1 || die "make failed" * The die message: * make failed * * If you need support, post the topmost build error, and the call stack if relevant. * A complete build log is located at '/var/tmp/portage/sci-mathematics/coq-8.2_p1-r1/temp/build.log'. * The ebuild environment file is located at '/var/tmp/portage/sci-mathematics/coq-8.2_p1-r1/temp/environment'. *